diff --git a/Bedrock/Word.v b/Bedrock/Word.v
index 8f5729642..0e8b8ab88 100644
--- a/Bedrock/Word.v
+++ b/Bedrock/Word.v
@@ -2,7 +2,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** Fixed precision machine words *)
 
 Require Import Coq.Arith.Arith
-        Coq.Arith.Div2
         Coq.NArith.NArith
         Coq.Bool.Bool
         Coq.ZArith.ZArith.
diff --git a/src/ADTRefinement/FixedPoint.v b/src/ADTRefinement/FixedPoint.v
index c32e56230..2c2138438 100644
--- a/src/ADTRefinement/FixedPoint.v
+++ b/src/ADTRefinement/FixedPoint.v
@@ -1,6 +1,8 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Fiat.ADT Fiat.ADTNotation.
 Require Export Fiat.Computation.FixComp.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Arith.PeanoNat.
 
 Import LeastFixedPointFun.
 
@@ -113,9 +115,8 @@ Lemma length_wf' : forall A len l,
 Proof.
   induction len; simpl; intros;
     constructor; intros.
-  contradiction (NPeano.Nat.nlt_0_r _ H).
+  contradiction (Nat.nlt_0_r _ H).
   apply IHlen.
-  Require Import Coq.ZArith.ZArith.
   omega.
 Qed.
 
diff --git a/src/CertifiedExtraction/Extraction/External/Lists.v b/src/CertifiedExtraction/Extraction/External/Lists.v
index 06ac5a7ea..71f11a836 100644
--- a/src/CertifiedExtraction/Extraction/External/Lists.v
+++ b/src/CertifiedExtraction/Extraction/External/Lists.v
@@ -5,7 +5,7 @@ Require Export Bedrock.Platform.Facade.examples.QsADTs.
 Lemma CompileEmpty_helper {A}:
   forall (lst : list A) (w : W),
     Programming.propToWord (lst = @nil A) w ->
-    ret (bool2w (EqNat.beq_nat (Datatypes.length lst) 0)) ↝ w.
+    ret (bool2w (Nat.eqb (Datatypes.length lst) 0)) ↝ w.
 Proof.
   unfold Programming.propToWord, IF_then_else in *.
   destruct lst; simpl in *; destruct 1; repeat cleanup; try discriminate; fiat_t.
@@ -15,7 +15,7 @@ Hint Resolve CompileEmpty_helper : call_helpers_db.
 
 Lemma ListEmpty_helper :
   forall {A} (seq: list A),
-    (EqNat.beq_nat (Datatypes.length seq) 0) = match seq with
+    (Nat.eqb (Datatypes.length seq) 0) = match seq with
                                                | nil => true
                                                | _ :: _ => false
                                                end.
diff --git a/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/TupleList.v b/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/TupleList.v
index 5fbbe9308..003d2d156 100644
--- a/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/TupleList.v
+++ b/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/TupleList.v
@@ -123,7 +123,7 @@ Module ADTListCompilation
       GLabelMap.MapsTo fpointer (Axiomatic Empty) env ->
       {{ tenv }}
         Call vtest fpointer (vlst :: nil)
-      {{ [[`vtest ->> (bool2w (EqNat.beq_nat (Datatypes.length lst) 0)) as _]] :: (DropName vtest tenv) }} ∪ {{ ext }} // env.
+      {{ [[`vtest ->> (bool2w (Nat.eqb (Datatypes.length lst) 0)) as _]] :: (DropName vtest tenv) }} ∪ {{ ext }} // env.
   Proof.
     repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || PreconditionSet_t || injections).
 
@@ -144,7 +144,7 @@ Module ADTListCompilation
       GLabelMap.MapsTo fpointer (Axiomatic Empty) env ->
       {{ tenv }}
         Call vtest fpointer (vlst :: nil)
-      {{ [[`vtest ->> (bool2w (EqNat.beq_nat (Datatypes.length (rev lst)) 0)) as _]] :: tenv }} ∪ {{ ext }} // env.
+      {{ [[`vtest ->> (bool2w (Nat.eqb (Datatypes.length (rev lst)) 0)) as _]] :: tenv }} ∪ {{ ext }} // env.
   Proof.
     intros.
     setoid_rewrite rev_length.
diff --git a/src/CertifiedExtraction/Extraction/QueryStructures/QueryStructures.v b/src/CertifiedExtraction/Extraction/QueryStructures/QueryStructures.v
index fa288da04..0d3a597c8 100644
--- a/src/CertifiedExtraction/Extraction/QueryStructures/QueryStructures.v
+++ b/src/CertifiedExtraction/Extraction/QueryStructures/QueryStructures.v
@@ -154,7 +154,7 @@ Ltac _compile_length :=
   match_ProgOk
     ltac:(fun prog pre post ext env =>
             match constr:((pre, post)) with
-            | (?pre, Cons ?k (ret (bool2w (EqNat.beq_nat (Datatypes.length (rev ?seq)) 0))) (fun _ => ?pre')) =>
+            | (?pre, Cons ?k (ret (bool2w (Nat.eqb (Datatypes.length (rev ?seq)) 0))) (fun _ => ?pre')) =>
               let vlst := find_fast (wrap (FacadeWrapper := WrapInstance (H := QS_WrapFiatWTupleList)) seq) ext in
               match vlst with
               | Some ?vlst => eapply (WTupleListCompilation.CompileEmpty_spec (idx := 3) (vlst := vlst))
diff --git a/src/Common.v b/src/Common.v
index 2d265ddeb..e3ea01bfa 100644
--- a/src/Common.v
+++ b/src/Common.v
@@ -1,5 +1,4 @@
 Require Import Coq.Lists.List.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith Coq.Lists.SetoidList.
 Require Export Coq.Setoids.Setoid Coq.Classes.RelationClasses
         Coq.Program.Program Coq.Classes.Morphisms.
@@ -1330,7 +1329,7 @@ Definition path_prod' {A B} {x x' : A} {y y' : B}
 
 Lemma lt_irrefl' {n m} (H : n = m) : ~n < m.
 Proof.
-  subst; apply Lt.lt_irrefl.
+  subst; apply Nat.lt_irrefl.
 Qed.
 
 Lemma or_not_l {A B} (H : A \/ B) (H' : ~A) : B.
@@ -1627,7 +1626,7 @@ Module opt.
   Definition snd {A B} := Eval compute in @snd A B.
   Definition andb := Eval compute in andb.
   Definition orb := Eval compute in orb.
-  Definition beq_nat := Eval compute in EqNat.beq_nat.
+  Definition beq_nat := Eval compute in Nat.eqb.
 
   Module Export Notations.
     Delimit Scope opt_bool_scope with opt_bool.
@@ -1641,7 +1640,7 @@ Module opt2.
   Definition snd {A B} := Eval compute in @snd A B.
   Definition andb := Eval compute in andb.
   Definition orb := Eval compute in orb.
-  Definition beq_nat := Eval compute in EqNat.beq_nat.
+  Definition beq_nat := Eval compute in Nat.eqb.
   Definition leb := Eval compute in Compare_dec.leb.
 
   Module Export Notations.
diff --git a/src/Common/BoundedLookup.v b/src/Common/BoundedLookup.v
index 29092d83f..cd6dd889a 100644
--- a/src/Common/BoundedLookup.v
+++ b/src/Common/BoundedLookup.v
@@ -141,7 +141,7 @@ Section BoundedIndex.
 
     Fixpoint fin_beq {m n} (p : Fin.t m) (q : Fin.t n) :=
       match p, q with
-      | @Fin.F1 m', @Fin.F1 n' => EqNat.beq_nat m' n'
+      | @Fin.F1 m', @Fin.F1 n' => Nat.eqb m' n'
       | Fin.FS _ _, Fin.F1 _ => false
       | Fin.F1 _, Fin.FS _ _ => false
       | Fin.FS _ p', Fin.FS _ q' => fin_beq p' q'
@@ -153,7 +153,7 @@ Section BoundedIndex.
     Proof.
       intros; pattern n, p, q; eapply Fin.rect2; simpl;
         intuition; try (congruence || discriminate).
-      - symmetry; eapply beq_nat_refl.
+      - eapply Nat.eqb_refl.
       - eauto using Fin.FS_inj.
     Qed.
 
diff --git a/src/Common/Enumerable.v b/src/Common/Enumerable.v
index 7dd3cee3c..df38dc10b 100644
--- a/src/Common/Enumerable.v
+++ b/src/Common/Enumerable.v
@@ -20,7 +20,7 @@ Section enum.
 
   Definition enumerate_fun_beq (enumerate : list A) (f g : A -> B)
   : bool
-    := EqNat.beq_nat (List.length (List.filter (fun x => negb (beq (f x) (g x))) enumerate)) 0.
+    := Nat.eqb (List.length (List.filter (fun x => negb (beq (f x) (g x))) enumerate)) 0.
 
   Definition enumerate_fun_bl_in
              (bl : forall x y, beq x y = true -> x = y)
@@ -29,7 +29,7 @@ Section enum.
   Proof.
     unfold enumerate_fun_beq.
     intros H x H'.
-    apply EqNat.beq_nat_true in H.
+    apply Nat.eqb_eq in H.
     apply bl.
     destruct (beq (f x) (g x)) eqn:Heq; [ reflexivity | exfalso ].
     apply Bool.negb_true_iff in Heq.
diff --git a/src/Common/Equality.v b/src/Common/Equality.v
index 450be0d26..ac9498281 100644
--- a/src/Common/Equality.v
+++ b/src/Common/Equality.v
@@ -1,5 +1,6 @@
 Require Import Coq.Lists.List Coq.Lists.SetoidList.
 Require Import Coq.Bool.Bool.
+Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
 Require Import Coq.Logic.Eqdep_dec.
@@ -379,10 +380,10 @@ Definition internal_prod_dec_lb {A B} eq_A eq_B A_lb B_lb x y
              H
              (surjective_pairing _))).
 
-Global Instance nat_BoolDecR : BoolDecR nat := EqNat.beq_nat.
-Global Instance nat_BoolDec_bl : BoolDec_bl (@eq nat) := @EqNat.beq_nat_true.
+Global Instance nat_BoolDecR : BoolDecR nat := Nat.eqb.
+Global Instance nat_BoolDec_bl : BoolDec_bl (@eq nat) := fun n m => (proj1 (Nat.eqb_eq n m)).
 Global Instance nat_BoolDec_lb : BoolDec_lb (@eq nat) :=
-  fun x y => proj2 (@EqNat.beq_nat_true_iff x y).
+  fun x y => proj2 (@Nat.eqb_eq x y).
 
 Lemma unit_bl {x y} : unit_beq x y = true -> x = y.
 Proof. apply internal_unit_dec_bl. Qed.
diff --git a/src/Common/FixedPoints.v b/src/Common/FixedPoints.v
index 3c6472f4f..2477f162b 100644
--- a/src/Common/FixedPoints.v
+++ b/src/Common/FixedPoints.v
@@ -62,7 +62,7 @@ Section fixedpoints.
              | _ => omega
              | [ H : forall a, _ -> _ = _ |- _ ] => rewrite H by omega
              | [ H : _ < _ |- _ ] => hnf in H
-             | [ H : S _ <= S _ |- _ ] => apply Le.le_S_n in H
+             | [ H : S _ <= S _ |- _ ] => apply Nat.succ_le_mono in H
              | [ H : sizeof ?x <= ?y, H' : ?y <= sizeof (step ?x) |- _ ]
                => let H'' := fresh in
                   assert (H'' : sizeof (step x) <= sizeof x) by apply step_monotonic;
@@ -95,7 +95,7 @@ Section listpair.
   Lemma step_monotonic lss : sizeof_pair (step lss) <= sizeof_pair lss.
   Proof.
     unfold step, sizeof_pair; simpl;
-      apply Plus.plus_le_compat;
+      apply Nat.add_le_mono;
       apply length_filter.
   Qed.
 
diff --git a/src/Common/Frame.v b/src/Common/Frame.v
index e2dafcb70..65681af97 100644
--- a/src/Common/Frame.v
+++ b/src/Common/Frame.v
@@ -1,7 +1,7 @@
 Require Import
         SetoidClass
-        Coq.Arith.Max
-        Coq.Classes.Morphisms.
+        Coq.Classes.Morphisms
+        Coq.Arith.PeanoNat.
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 
 Generalizable All Variables.
@@ -212,7 +212,7 @@ Module PreO.
   Qed.
 
   Definition Nat : t le.
-  Proof. constructor; [ apply Le.le_refl | apply Le.le_trans ].
+  Proof. constructor; [ apply Nat.le_refl | apply Nat.le_trans ].
   Qed.
 
   Definition discrete (A : Type) : t (@Logic.eq A).
@@ -408,7 +408,7 @@ Module PO.
     constructor; intros.
     - apply PreO.Nat.
     - solve_proper.
-    - apply Le.le_antisym; assumption.
+    - apply Nat.le_antisymm; assumption.
   Qed.
 
   Definition discrete (A : Type) : t (@Logic.eq A) Logic.eq.
@@ -585,8 +585,8 @@ Module JoinLat.
   Proof. constructor; intros.
          - apply PO.Nat.
          - solve_proper.
-         - constructor. simpl. apply Max.le_max_l. apply Max.le_max_r.
-           apply Max.max_lub.
+         - constructor. simpl. apply Nat.le_max_l. apply Nat.le_max_r.
+           apply Nat.max_lub.
   Qed.
 
   (** Max for propositions is the propositional OR, i.e., disjunction *)
diff --git a/src/Common/Le.v b/src/Common/Le.v
index 08b893fc1..980bb9c12 100644
--- a/src/Common/Le.v
+++ b/src/Common/Le.v
@@ -1,6 +1,5 @@
 (** * Common facts about [≤] *)
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
-Require Import Coq.Arith.Le.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
@@ -46,7 +45,7 @@ Proof.
   induction n; simpl; try reflexivity.
   rewrite IHn; clear IHn.
   edestruct le_canonical; [ exfalso | reflexivity ].
-  { eapply le_Sn_n; eassumption. }
+  { eapply Nat.nle_succ_diag_l; eassumption. }
 Qed.
 
 Lemma le_canonical_nS {n m pf} (H : le_canonical n m = left pf)
@@ -103,13 +102,13 @@ Proof. omega. Qed.
 Global Instance le_lt_Proper : Proper (Basics.flip le ==> le ==> impl) lt.
 Proof.
   repeat intro.
-  eapply lt_le_trans; [ | eassumption ].
-  eapply le_lt_trans; eassumption.
+  eapply Nat.lt_le_trans; [ | eassumption ].
+  eapply Nat.le_lt_trans; eassumption.
 Qed.
 
 Global Instance le_lt_Proper' : Proper (le ==> Basics.flip le ==> Basics.flip impl) lt.
 Proof.
   repeat intro.
-  eapply lt_le_trans; [ | eassumption ].
-  eapply le_lt_trans; eassumption.
+  eapply Nat.lt_le_trans; [ | eassumption ].
+  eapply Nat.le_lt_trans; eassumption.
 Qed.
diff --git a/src/Common/List/FlattenList.v b/src/Common/List/FlattenList.v
index 42eebb587..74c46cd3e 100644
--- a/src/Common/List/FlattenList.v
+++ b/src/Common/List/FlattenList.v
@@ -92,7 +92,7 @@ Section FlattenList.
     - auto with arith.
     - unfold compose;
       rewrite app_length, <- IHseq.
-      rewrite plus_comm, <- plus_assoc; auto with arith.
+      rewrite Nat.add_comm, <- Nat.add_assoc; auto with arith.
   Qed.
 
   Lemma length_flatten :
diff --git a/src/Common/List/ListFacts.v b/src/Common/List/ListFacts.v
index e54018e02..09c578432 100644
--- a/src/Common/List/ListFacts.v
+++ b/src/Common/List/ListFacts.v
@@ -351,8 +351,8 @@ Section ListFacts.
     clear IHseq; revert a default; induction seq;
       simpl; intros; auto with arith.
     rewrite <- IHseq.
-    rewrite Plus.plus_comm, <- Plus.plus_assoc; f_equal.
-    rewrite Plus.plus_comm; reflexivity.
+    rewrite Nat.add_comm, <- Nat.add_assoc; f_equal.
+    rewrite Nat.add_comm; reflexivity.
   Qed.
 
   Lemma map_snd {A B C} :
@@ -433,7 +433,7 @@ Section ListFacts.
   Proof.
     induction seq; simpl; intros; eauto with arith.
     rewrite IHseq; f_equal; eauto with arith.
-    repeat rewrite <- Plus.plus_assoc; f_equal; auto with arith.
+    repeat rewrite <- Nat.add_assoc; f_equal; auto with arith.
   Qed.
 
   Lemma length_flat_map :
@@ -603,7 +603,7 @@ Section ListFacts.
     { destruct y; simpl.
       { destruct x; simpl; repeat (f_equal; []); try reflexivity; omega. }
       { rewrite IHls; destruct x; simpl; repeat (f_equal; []); try reflexivity.
-        rewrite NPeano.Nat.add_succ_r; reflexivity. } }
+        rewrite Nat.add_succ_r; reflexivity. } }
   Qed.
 
   Lemma in_map_iffT' {A B}
@@ -639,7 +639,7 @@ Section ListFacts.
         (f : A -> nat) (ls : list A) (y : nat)
     : iffT (In y (map f ls)) { x : A | f x = y /\ In x ls }.
   Proof.
-    apply in_map_iffT, NPeano.Nat.eq_dec.
+    apply in_map_iffT, Nat.eq_dec.
   Defined.
 
   Lemma nth_take_1_drop {A} (ls : list A) n a
@@ -670,7 +670,7 @@ Section ListFacts.
     : drop 1 (drop y ls) = drop (S y) ls.
   Proof.
     rewrite drop_drop.
-    rewrite NPeano.Nat.add_1_r.
+    rewrite Nat.add_1_r.
     reflexivity.
   Qed.
 
@@ -967,7 +967,7 @@ Section ListFacts.
        | [ H : context[option_map _ ?x] |- _ ] => destruct x eqn:?; unfold option_map in H
        | _ => solve [ repeat (esplit || eassumption) ]
        | [ H : context[nth_error (_::_) ?x] |- _ ] => is_var x; destruct x; simpl nth_error in H
-       | [ H : S _ < S _ |- _ ] => apply lt_S_n in H
+       | [ H : S _ < S _ |- _ ] => apply (proj2 (Nat.succ_lt_mono _ _)) in H
        | _ => solve [ eauto with nocore ]
        | [ |- context[if ?b then _ else _] ] => destruct b eqn:?
        | [ H : ?A -> ?B |- _ ] => let H' := fresh in assert (H' : A) by (assumption || omega); specialize (H H'); clear H'
@@ -975,7 +975,7 @@ Section ListFacts.
        | _ => progress simpl in *
        | [ H : forall x, ?f x = ?f ?y -> _ |- _ ] => specialize (H _ eq_refl)
        | [ H : forall x, ?f ?y = ?f x -> _ |- _ ] => specialize (H _ eq_refl)
-       | [ H : forall n, S n < S _ -> _ |- _ ] => specialize (fun n pf => H n (lt_n_S _ _ pf))
+       | [ H : forall n, S n < S _ -> _ |- _ ] => specialize (fun n pf => H n (proj1 (Nat.succ_lt_mono _ _) pf))
        | [ H : nth_error nil ?x = Some _ |- _ ] => is_var x; destruct x
        | [ H : forall m x, nth_error (_::_) m = Some _ -> _ |- _ ] => pose proof (H 0); specialize (fun m => H (S m))
        | [ H : or _ _ |- _ ] => destruct H
@@ -1106,11 +1106,11 @@ Section ListFacts.
     induction ls as [|x xs IHxs].
     { simpl; intros; destruct (n - offset); reflexivity. }
     { simpl; intros.
-      destruct (beq_nat n offset) eqn:H';
-        [ apply beq_nat_true in H'
-        | apply beq_nat_false in H' ];
+      destruct (Nat.eqb n offset) eqn:H';
+        [ apply Nat.eqb_eq in H'
+        | apply Nat.eqb_neq in H' ];
         subst;
-        rewrite ?minus_diag; trivial.
+        rewrite ?Nat.sub_diag; trivial.
       destruct (n - offset) eqn:H''.
       { omega. }
       { rewrite IHxs by omega.
@@ -1997,7 +1997,7 @@ Section ListFacts.
       List.In n ns -> f n <= fold_right (fun n acc => max (f n) acc) 0 ns.
   Proof.
     induction ns; intros; inversion H; subst; simpl;
-      apply NPeano.Nat.max_le_iff; [ left | right ]; auto.
+      apply Nat.max_le_iff; [ left | right ]; auto.
   Qed.
 
   Lemma fold_right_higher_is_higher {A}
@@ -2006,7 +2006,7 @@ Section ListFacts.
       fold_right (fun n acc => max (f n) acc) 0 ns <= x.
   Proof.
     induction ns; simpl; intros; [ apply le_0_n | ].
-    apply NPeano.Nat.max_lub.
+    apply Nat.max_lub.
     apply H; left; auto.
     apply IHns; intros; apply H; right; auto.
   Qed.
@@ -2023,8 +2023,8 @@ Section ListFacts.
   (* if a list is empty, the result of filtering the list with anything will still be empty *)
   Lemma filter_nil_is_nil {A}
     : forall (l : list A) (pred : A -> bool),
-      beq_nat (Datatypes.length l) 0 = true
-      ->  beq_nat (Datatypes.length (filter pred l)) 0 = true.
+      Nat.eqb (Datatypes.length l) 0 = true
+      ->  Nat.eqb (Datatypes.length (filter pred l)) 0 = true.
   Proof.
     induction l; intros; simpl; try inversion H.
     reflexivity.
@@ -2374,7 +2374,7 @@ Section ListFacts.
       = option_map (fun v => (start + idx, v)) (nth_error ls idx).
   Proof.
     revert start idx; induction ls as [|l ls IHls], idx as [|idx]; try reflexivity.
-    { simpl; rewrite NPeano.Nat.add_0_r; reflexivity. }
+    { simpl; rewrite Nat.add_0_r; reflexivity. }
     { simpl; rewrite <- plus_n_Sm, IHls; reflexivity. }
   Qed.
 
diff --git a/src/Common/List/Operations.v b/src/Common/List/Operations.v
index 5669d0fae..e3100b877 100644
--- a/src/Common/List/Operations.v
+++ b/src/Common/List/Operations.v
@@ -74,7 +74,7 @@ Module Export List.
   Fixpoint nth'_helper {A} (n : nat) (ls : list A) (default : A) (offset : nat) :=
     match ls with
       | nil => default
-      | x::xs => if EqNat.beq_nat n offset
+      | x::xs => if Nat.eqb n offset
                  then x
                  else nth'_helper n xs default (S offset)
     end.
diff --git a/src/Common/NatFacts.v b/src/Common/NatFacts.v
index 1a33852cb..724dfb4cd 100644
--- a/src/Common/NatFacts.v
+++ b/src/Common/NatFacts.v
@@ -1,12 +1,11 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Coq.Classes.Morphisms.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
 
 Lemma min_def {x y} : min x y = x - (x - y).
-Proof. apply Min.min_case_strong; omega. Qed.
+Proof. apply Nat.min_case_strong; omega. Qed.
 Lemma max_def {x y} : max x y = x + (y - x).
-Proof. apply Max.max_case_strong; omega. Qed.
+Proof. apply Nat.max_case_strong; omega. Qed.
 Ltac coq_omega := omega.
 Ltac handle_min_max_for_omega :=
   repeat match goal with
@@ -19,8 +18,8 @@ Ltac handle_min_max_for_omega_case :=
   repeat match goal with
          | [ H : context[min _ _] |- _ ] => revert H
          | [ H : context[max _ _] |- _ ] => revert H
-         | [ |- context[min _ _] ] => apply Min.min_case_strong
-         | [ |- context[max _ _] ] => apply Max.max_case_strong
+         | [ |- context[min _ _] ] => apply Nat.min_case_strong
+         | [ |- context[max _ _] ] => apply Nat.max_case_strong
          end;
   intros.
 Ltac omega_with_min_max :=
@@ -59,9 +58,9 @@ Section NatFacts.
 
   Lemma beq_nat_eq_nat_dec :
     forall x y,
-      beq_nat x y = if eq_nat_dec x y then true else false.
+      Nat.eqb x y = if eq_nat_dec x y then true else false.
   Proof.
-    intros; destruct (eq_nat_dec _ _); [ apply beq_nat_true_iff | apply beq_nat_false_iff ]; assumption.
+    intros; destruct (eq_nat_dec _ _); [ apply Nat.eqb_eq | apply Nat.eqb_neq ]; assumption.
   Qed.
 
   Lemma min_minus_l x y
@@ -110,7 +109,7 @@ Section dec_prod.
   Proof.
     destruct max as [|max];
     [ clear dec_stabalize' | specialize (dec_stabalize' max) ].
-    { destruct (Hdec 0 (le_refl _)) as [Hd|Hd]; [ left | right ].
+    { destruct (Hdec 0 (Nat.le_refl _)) as [Hd|Hd]; [ left | right ].
       { intro n.
         induction n as [|n IHn].
         { assumption. }
@@ -140,7 +139,7 @@ Section dec_prod.
   Proof.
     destruct max as [|max];
     [ clear dec_stabalize | specialize (dec_stabalize max) ].
-    { destruct (Hdec 0 (le_refl _)) as [Hd|Hd]; [ left | right ].
+    { destruct (Hdec 0 (Nat.le_refl _)) as [Hd|Hd]; [ left | right ].
       { exists 0; split; [ reflexivity | assumption ]. }
       { intros n Pn. apply Hd.
         clear -Pn Hstable.
@@ -196,8 +195,8 @@ Lemma min_case_strong_r n m (P : nat -> Type)
 : (n <= m -> P n) -> (m < n -> P m) -> P (min n m).
 Proof.
   destruct (Compare_dec.le_lt_dec n m);
-  first [ rewrite Min.min_r by omega
-        | rewrite Min.min_l by omega ];
+  first [ rewrite Nat.min_r by omega
+        | rewrite Nat.min_l by omega ];
   auto.
 Qed.
 
@@ -205,19 +204,19 @@ Lemma min_case_strong_l n m (P : nat -> Type)
 : (n < m -> P n) -> (m <= n -> P m) -> P (min n m).
 Proof.
   destruct (Compare_dec.le_lt_dec m n);
-  first [ rewrite Min.min_r by omega
-        | rewrite Min.min_l by omega ];
+  first [ rewrite Nat.min_r by omega
+        | rewrite Nat.min_l by omega ];
   auto.
 Qed.
 
 Lemma beq_0_1_leb x
-: (EqNat.beq_nat x 1 || EqNat.beq_nat x 0)%bool = Compare_dec.leb x 1.
+: (Nat.eqb x 1 || Nat.eqb x 0)%bool = Compare_dec.leb x 1.
 Proof.
   destruct x as [|[|]]; simpl; reflexivity.
 Qed.
 
 Lemma beq_S_leb x n
-: (EqNat.beq_nat x (S n) || Compare_dec.leb x n)%bool = Compare_dec.leb x (S n).
+: (Nat.eqb x (S n) || Compare_dec.leb x n)%bool = Compare_dec.leb x (S n).
 Proof.
   revert x; induction n as [|n IHn]; simpl.
   { intros [|[|]]; reflexivity. }
@@ -246,7 +245,7 @@ Lemma min_subr_same {x y} : (min x y - x)%natr = 0.
 Proof. clear; rewrite minusr_minus; omega *. Qed.
 
 Lemma beq_nat_min_0 {x y}
-  : EqNat.beq_nat (min x y) 0 = orb (EqNat.beq_nat x 0) (EqNat.beq_nat y 0).
+  : Nat.eqb (min x y) 0 = orb (Nat.eqb x 0) (Nat.eqb y 0).
 Proof. destruct x, y; simpl; reflexivity. Qed.
 
 Lemma max_min_n {x y} : max (min x y) y = y.
diff --git a/src/Common/StringFacts.v b/src/Common/StringFacts.v
index e14e4f912..10b7aca73 100644
--- a/src/Common/StringFacts.v
+++ b/src/Common/StringFacts.v
@@ -1,8 +1,8 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Fiat.Common.List.Operations.
 Require Import Fiat.Common.StringOperations.
 
@@ -23,10 +23,10 @@ Proof.
   induction s; simpl.
   { intros; destruct m; trivial. }
   { intros; destruct m.
-    { apply Lt.lt_n_0 in H.
+{ apply Nat.nlt_0_r in H.
       destruct H. }
     { rewrite IHs; trivial.
-      apply Le.le_S_n; trivial. } }
+      apply Nat.succ_le_mono; trivial. } }
 Qed.
 
 Lemma substring_correct3' {s : string}
@@ -47,7 +47,7 @@ Proof.
   revert n m H; induction s; simpl; intros n m H.
   { destruct n, m; trivial. }
   { destruct n, m; trivial.
-    { apply le_Sn_0 in H; destruct H. }
+    { apply Nat.nlt_0_r in H; destruct H. }
     { rewrite IHs; eauto with arith. }
     { rewrite IHs; eauto with arith. } }
 Qed.
@@ -60,14 +60,15 @@ Proof.
   induction s; simpl in *.
   { intros; destruct m, m', n; trivial. }
   { intros; destruct m, m', n; trivial; simpl in *;
-    try (apply Lt.lt_n_0 in H; destruct H);
-    try (apply Lt.lt_n_0 in H'; destruct H');
-    try apply Le.le_S_n in H;
-    try apply Le.le_S_n in H';
-    try solve [ try rewrite plus_comm in H;
-                try rewrite plus_comm in H';
+    try (apply Nat.nlt_0_r in H; destruct H);
+    try (apply Nat.nlt_0_r in H'; destruct H');
+    try apply le_S_n in H;
+    try apply le_S_n in H';
+    try solve [ try rewrite Nat.add_comm in H;
+                try rewrite Nat.add_comm in H';
                 simpl in *;
                 rewrite !substring_correct0' by auto with arith; trivial ].
+                
     { apply f_equal.
       apply IHs; trivial. }
     { apply IHs; trivial. } }
@@ -90,7 +91,7 @@ Proof.
   induction s; simpl; intros.
   { destruct (y + z), x, y, z; reflexivity. }
   { destruct x, y, z; try reflexivity; simpl;
-    rewrite ?plus_0_r, ?substring_correct0, ?string_concat_empty_r;
+    rewrite ?Nat.add_0_r, ?substring_correct0, ?string_concat_empty_r;
     try reflexivity.
     { apply f_equal.
       apply IHs. }
@@ -151,14 +152,14 @@ Proof.
   induction s; intros.
   { destruct n, m, n', m'; reflexivity. }
   { destruct n', m';
-    rewrite <- ?plus_n_O, <- ?minus_n_O, ?Min.min_0_r, ?Min.min_0_l;
+    rewrite <- ?Nat.add_0_r, <- ?Nat.sub_0_r, ?Nat.min_0_r, ?Nat.min_0_l;
     destruct n, m;
     trivial; simpl;
-    rewrite ?IHs, ?substring_correct0, <- ?plus_n_O, <- ?minus_n_O;
+    rewrite ?IHs, ?substring_correct0, <- ?plus_n_O, ?Nat.sub_0_r;
     simpl;
     try reflexivity.
-    rewrite (plus_comm _ (S _)); simpl.
-    rewrite (plus_comm n n').
+    rewrite (Nat.add_comm _ (S _)); simpl.
+    rewrite (Nat.add_comm n n').
     reflexivity. }
 Qed.
 
@@ -178,7 +179,7 @@ Lemma substring_min {x x' y y' z str} (H : substring x y str = substring x' y' s
 Proof.
   pose proof (fun y x => @substring_substring str 0 z x y) as H'; simpl in *.
   setoid_rewrite Nat.sub_0_r in H'.
-  setoid_rewrite Min.min_comm in H'.
+  setoid_rewrite Nat.min_comm in H'.
   rewrite <- !H', H; reflexivity.
 Qed.
 
@@ -232,7 +233,7 @@ Qed.
 Lemma substring_min_length str x y
 : substring x (min y (length str)) str = substring x y str.
 Proof.
-  apply Min.min_case_strong; try reflexivity.
+  apply Nat.min_case_strong; try reflexivity.
   intro H.
   apply substring_correct4; omega.
 Qed.
diff --git a/src/Common/Wf.v b/src/Common/Wf.v
index d097c4682..9be4543dc 100644
--- a/src/Common/Wf.v
+++ b/src/Common/Wf.v
@@ -1,6 +1,7 @@
 (** * Miscellaneous Well-Foundedness Facts *)
 Require Import Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf.
 Require Import Coq.Lists.SetoidList.
+Require Import Coq.Arith.PeanoNat.
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 
 Set Implicit Arguments.
@@ -447,8 +448,8 @@ Section wf.
          | S n' => prod_relationA eqA R (@iterated_prod_relationA n')
          end.
 
-    Fixpoint nat_eq_transfer (P : nat -> Type) (n m : nat) : P n -> (P m) + (EqNat.beq_nat n m = false)
-      := match n, m return P n -> (P m) + (EqNat.beq_nat n m = false) with
+    Fixpoint nat_eq_transfer (P : nat -> Type) (n m : nat) : P n -> (P m) + (Nat.eqb n m = false)
+      := match n, m return P n -> (P m) + (Nat.eqb n m = false) with
          | 0, 0 => fun x => inl x
          | S n', S m' => @nat_eq_transfer (fun v => P (S v)) n' m'
          | _, _ => fun _ => inr eq_refl
@@ -461,11 +462,11 @@ Section wf.
          end.
 
     Fixpoint nat_eq_transfer_neq (P : nat -> Type) (n m : nat)
-      : forall v : P n, (if EqNat.beq_nat n m as b return ((P m) + (b = false)) -> Prop
+      : forall v : P n, (if Nat.eqb n m as b return ((P m) + (b = false)) -> Prop
                          then fun _ => True
                          else fun v => v = inr eq_refl)
                           (nat_eq_transfer P n m v)
-      := match n, m return forall v : P n, (if EqNat.beq_nat n m as b return ((P m) + (b = false)) -> Prop
+      := match n, m return forall v : P n, (if Nat.eqb n m as b return ((P m) + (b = false)) -> Prop
                                             then fun _ => True
                                             else fun v => v = inr eq_refl)
                                              (nat_eq_transfer P n m v)
@@ -521,8 +522,8 @@ Section wf.
                             cbv beta in *;
                             generalize dependent (nat_eq_transfer iterated_prod n1' n0');
                             let Heq := fresh in
-                            destruct (EqNat.beq_nat n1' n0') eqn:Heq;
-                            [ apply EqNat.beq_nat_true_iff in Heq; subst; rewrite <- EqNat.beq_nat_refl in H;
+                            destruct (Nat.eqb n1' n0') eqn:Heq;
+                            [ apply Nat.eqb_eq in Heq; subst; rewrite Nat.eqb_refl in H;
                               exfalso; clear -H; congruence
                             | ]
                        | [ |- context[@nat_eq_transfer iterated_prod n0' n1' _] ]
diff --git a/src/Computation/Decidable.v b/src/Computation/Decidable.v
index b3f7929f7..027d6d4c6 100644
--- a/src/Computation/Decidable.v
+++ b/src/Computation/Decidable.v
@@ -150,9 +150,9 @@ Obligation 1. t; destruct (Ascii.ascii_dec n m); auto; discriminate. Qed.
 Require Import Coq.Arith.Arith.
 
 Global Program Instance nat_eq_Decidable {n m : nat} : Decidable (n = m) := {
-  Decidable_witness := beq_nat n m
+  Decidable_witness := Nat.eqb n m
 }.
-Obligation 1. t' beq_nat_true_iff. Qed.
+Obligation 1. t' Nat.eqb_eq. Qed.
 
 Global Program Instance le_Decidable {n m} : Decidable (Nat.le n m) := {
   Decidable_witness := Compare_dec.leb n m
diff --git a/src/Computation/ListComputations.v b/src/Computation/ListComputations.v
index e1a1ff0e8..8f160c4b3 100644
--- a/src/Computation/ListComputations.v
+++ b/src/Computation/ListComputations.v
@@ -107,14 +107,14 @@ Section UpperBound.
   Definition find_UpperBound (f : A -> nat) (ns : list A) : list A :=
     let max := fold_right
                  (fun n acc => max (f n) acc) O ns in
-    filter (fun n => NPeano.Nat.leb max (f n)) ns.
+    filter (fun n => Nat.leb max (f n)) ns.
 
   Lemma find_UpperBound_highest_length
     : forall (f : A -> nat) ns n,
       List.In n (find_UpperBound f ns) -> forall n', List.In n' ns -> (f n) >= (f n').
   Proof.
     unfold ge, find_UpperBound; intros.
-    apply filter_In in H; destruct H. apply NPeano.Nat.leb_le in H1.
+    apply filter_In in H; destruct H. apply Nat.leb_le in H1.
     rewrite <- H1; clear H1 H n.
     apply fold_right_max_is_max; auto.
   Qed.
@@ -127,9 +127,9 @@ Instance DecideableEnsembleUpperBound {A}
          (ns : list A)
   : DecideableEnsemble (UpperBound (fun a a' => f a <= f a') ns).
 Proof.
-refine {| dec n := NPeano.Nat.leb (fold_right (fun n acc => max (f n) acc) O ns) (f n) |}.
-  unfold UpperBound, ge; intros; rewrite NPeano.Nat.leb_le; intuition.
-  - remember (f a); clear Heqn; subst; eapply le_trans;
+refine {| dec n := Nat.leb (fold_right (fun n acc => max (f n) acc) O ns) (f n) |}.
+  unfold UpperBound, ge; intros; rewrite Nat.leb_le; intuition.
+  - remember (f a); clear Heqn; subst; eapply Nat.le_trans;
       [ apply fold_right_max_is_max; apply H0 | assumption ].
   - eapply fold_right_higher_is_higher; eauto.
 Defined.
diff --git a/src/Narcissus/Automation/Decision.v b/src/Narcissus/Automation/Decision.v
index f0c9dfb07..583b75148 100644
--- a/src/Narcissus/Automation/Decision.v
+++ b/src/Narcissus/Automation/Decision.v
@@ -50,12 +50,12 @@ Qed.
 
 Lemma decides_nat_eq :
   forall (n n' : nat),
-    decides (EqNat.beq_nat n n') (n = n').
+    decides (Nat.eqb n n') (n = n').
 Proof.
   unfold decides, If_Then_Else; intros.
-  destruct (EqNat.beq_nat n n') eqn: ? ;
-    try eapply EqNat.beq_nat_true_iff;
-    try eapply EqNat.beq_nat_false_iff; eauto.
+  destruct (Nat.eqb n n') eqn: ? ;
+    try eapply Nat.eqb_true_iff;
+    try eapply Nat.eqb_false_iff; eauto.
 Qed.
 
 Lemma decides_word_eq {sz}:
diff --git a/src/Parsers/BaseTypesLemmas.v b/src/Parsers/BaseTypesLemmas.v
index da64a787c..340a95630 100644
--- a/src/Parsers/BaseTypesLemmas.v
+++ b/src/Parsers/BaseTypesLemmas.v
@@ -112,13 +112,13 @@ Section recursive_descent_parser.
   Lemma nonempty_nonterminals {ls nt} (H : is_valid_nonterminal ls nt)
   : 0 < nonterminals_length ls.
   Proof.
-    eapply Lt.le_lt_trans;
-    [ apply Le.le_0_n
+    eapply Nat.le_lt_trans;
+    [ apply Nat.le_0_l
     | exact (remove_nonterminal_dec ls nt H) ].
   Qed.
 
   Lemma nonempty_nonterminals' {ls nt} (H : is_valid_nonterminal ls nt)
-  : negb (EqNat.beq_nat (nonterminals_length ls) 0).
+  : negb (Nat.eqb (nonterminals_length ls) 0).
   Proof.
     pose proof (nonempty_nonterminals H).
     destruct (nonterminals_length ls); simpl; try reflexivity; try omega.
diff --git a/src/Parsers/BooleanRecognizerOptimized.v b/src/Parsers/BooleanRecognizerOptimized.v
index eb562e417..d952d3bb7 100644
--- a/src/Parsers/BooleanRecognizerOptimized.v
+++ b/src/Parsers/BooleanRecognizerOptimized.v
@@ -58,7 +58,7 @@ Module Export opt.
     Definition hd {A} := Eval compute in @hd A.
     Definition tl {A} := Eval compute in @tl A.
     Definition nth {A} := Eval compute in @nth A.
-    Definition nth' {A} := Eval cbv beta iota zeta delta -[EqNat.beq_nat] in @nth' A.
+    Definition nth' {A} := Eval cbv beta iota zeta delta -[Nat.eqb] in @nth' A.
     Definition fst {A B} := Eval compute in @fst A B.
     Definition snd {A B} := Eval compute in @snd A B.
     Definition list_caset {A} := Eval compute in @list_caset A.
@@ -68,7 +68,7 @@ Module Export opt.
     Definition pred := Eval compute in pred.
     Definition minusr := Eval compute in minusr.
     Definition id {A} := Eval compute in @id A.
-    Definition beq_nat := Eval compute in EqNat.beq_nat.
+    Definition beq_nat := Eval compute in Nat.eqb.
     Definition leb := Eval compute in Compare_dec.leb.
     Definition interp_RCharExpr {Char idata} := Eval cbv -[andb orb negb Compare_dec.leb] in @interp_RCharExpr Char idata.
   End opt.
@@ -94,7 +94,7 @@ Module Export opt2.
     Definition hd {A} := Eval compute in @hd A.
     Definition tl {A} := Eval compute in @tl A.
     Definition nth {A} := Eval compute in @nth A.
-    Definition nth' {A} := Eval cbv beta iota zeta delta -[EqNat.beq_nat] in @nth' A.
+    Definition nth' {A} := Eval cbv beta iota zeta delta -[Nat.eqb] in @nth' A.
     Definition fst {A B} := Eval compute in @fst A B.
     Definition snd {A B} := Eval compute in @snd A B.
     Definition list_caset {A} := Eval compute in @list_caset A.
@@ -104,7 +104,7 @@ Module Export opt2.
     Definition pred := Eval compute in pred.
     Definition minusr := Eval compute in minusr.
     Definition id {A} := Eval compute in @id A.
-    Definition beq_nat := Eval compute in EqNat.beq_nat.
+    Definition beq_nat := Eval compute in Nat.eqb.
     Definition leb := Eval compute in Compare_dec.leb.
     Definition interp_RCharExpr {Char idata} := Eval cbv -[andb orb negb Compare_dec.leb] in @interp_RCharExpr Char idata.
   End opt2.
@@ -130,7 +130,7 @@ Module Export opt3.
     Definition hd {A} := Eval compute in @hd A.
     Definition tl {A} := Eval compute in @tl A.
     Definition nth {A} := Eval compute in @nth A.
-    Definition nth' {A} := Eval cbv beta iota zeta delta -[EqNat.beq_nat] in @nth' A.
+    Definition nth' {A} := Eval cbv beta iota zeta delta -[Nat.eqb] in @nth' A.
     Definition fst {A B} := Eval compute in @fst A B.
     Definition snd {A B} := Eval compute in @snd A B.
     Definition list_caset {A} := Eval compute in @list_caset A.
@@ -140,7 +140,7 @@ Module Export opt3.
     Definition pred := Eval compute in pred.
     Definition minusr := Eval compute in minusr.
     Definition id {A} := Eval compute in @id A.
-    Definition beq_nat := Eval compute in EqNat.beq_nat.
+    Definition beq_nat := Eval compute in Nat.eqb.
     Definition leb := Eval compute in Compare_dec.leb.
     Definition interp_RCharExpr {Char idata} := Eval cbv -[andb orb negb Compare_dec.leb] in @interp_RCharExpr Char idata.
   End opt3.
@@ -271,9 +271,9 @@ Section recursive_descent_parser.
              | [ H : (_ && _)%bool = true |- _ ] => apply Bool.andb_true_iff in H
              | [ H : _ = in_left |- _ ] => clear H
              | [ H : _ /\ _ |- _ ] => destruct H
-             | [ H : context[negb (EqNat.beq_nat ?x ?y)] |- _ ] => destruct (EqNat.beq_nat x y) eqn:?
-             | [ H : EqNat.beq_nat _ _ = false |- _ ] => apply EqNat.beq_nat_false in H
-             | [ H : EqNat.beq_nat _ _ = true |- _ ] => apply EqNat.beq_nat_true in H
+             | [ H : context[negb (Nat.eqb ?x ?y)] |- _ ] => destruct (Nat.eqb x y) eqn:?
+             | [ H : Nat.eqb _ _ = false |- _ ] => apply Nat.eqb_false in H
+             | [ H : Nat.eqb _ _ = true |- _ ] => apply Nat.eqb_true in H
              | [ H : snd ?x = _ |- _ ] => is_var x; destruct x
              | _ => progress simpl negb in *
              | [ H : false = true |- _ ] => inversion H
@@ -425,7 +425,7 @@ Section recursive_descent_parser.
              | [ |- _ = 0 ] => reflexivity
              | [ |- _ = 1 ] => reflexivity
              | [ |- _ = None ] => reflexivity
-             | [ |- _ = EqNat.beq_nat _ _ ] => apply f_equal2
+             | [ |- _ = Nat.eqb _ _ ] => apply f_equal2
              | [ |- _ = Compare_dec.leb _ _ ] => apply f_equal2
              | [ |- _ = S _ ] => apply f_equal
              | [ |- _ = string_beq _ _ ] => apply f_equal2
@@ -1159,7 +1159,7 @@ Section recursive_descent_parser.
                                               (fun _ => _)
                                               (N0 a' b' c')
                                               (list_rect P0 (fun _ _ _ => true) C0 ls' a' b' c')
-                                              (EqNat.beq_nat (List.length ls') 0))
+                                              (Nat.eqb (List.length ls') 0))
                                            = list_rect P0 N0 C0 ls' a' b' c')
                              _
                              _
@@ -1193,11 +1193,11 @@ Section recursive_descent_parser.
                      | _ => progress simpl
                      | [ |- ?x = ?x ] => reflexivity
                      | _ => progress rewrite ?Bool.andb_true_r, ?Min.min_idempotent, ?Minus.minus_diag
-                     | [ H : EqNat.beq_nat _ _ = true |- _ ]
-                       => apply EqNat.beq_nat_true in H
+                     | [ H : Nat.eqb _ _ = true |- _ ]
+                       => apply Nat.eqb_true in H
                      | _ => progress subst
-                     | [ |- context[EqNat.beq_nat ?x ?y] ]
-                       => is_var x; destruct (EqNat.beq_nat x y) eqn:?
+                     | [ |- context[Nat.eqb ?x ?y] ]
+                       => is_var x; destruct (Nat.eqb x y) eqn:?
                      | [ H := _ |- _ ] => subst H
                      | [ |- context[orb _ false] ] => rewrite Bool.orb_false_r
                      | _ => rewrite minusr_minus
@@ -1252,7 +1252,7 @@ Section recursive_descent_parser.
                 step_opt'; [].
                 apply (f_equal2 andb); [ | reflexivity ].
                 match goal with
-                | [ |- _ = EqNat.beq_nat (min ?v ?x) ?v ]
+                | [ |- _ = Nat.eqb (min ?v ?x) ?v ]
                   => refine (_ : Compare_dec.leb v x = _)
                 end.
                 match goal with
@@ -1418,13 +1418,13 @@ Section recursive_descent_parser.
             rewrite bool_rect_andb; simpl.
             rewrite Bool.andb_true_r.
             match goal with
-            | [ |- _ = (orb (negb (EqNat.beq_nat ?x 0)) (andb (EqNat.beq_nat ?x 0) ?y)) ]
+            | [ |- _ = (orb (negb (Nat.eqb ?x 0)) (andb (Nat.eqb ?x 0) ?y)) ]
               => let z := fresh in
                  let y' := fresh in
                  set (z := x);
                    set (y' := y);
                    refine (_ : orb (Compare_dec.leb 1 x) y = _);
-                   change (orb (Compare_dec.leb 1 z) y' = orb (negb (EqNat.beq_nat z 0)) (andb (EqNat.beq_nat z 0) y'));
+                   change (orb (Compare_dec.leb 1 z) y' = orb (negb (Nat.eqb z 0)) (andb (Nat.eqb z 0) y'));
                    destruct z, y'; reflexivity
             end. }
           etransitivity_rev _.
@@ -1627,13 +1627,13 @@ Section recursive_descent_parser.
           { rewrite bool_rect_andb.
             rewrite Bool.andb_true_r.
             match goal with
-            | [ |- _ = (orb (negb (EqNat.beq_nat ?x 0)) (andb (EqNat.beq_nat ?x 0) ?y)) ]
+            | [ |- _ = (orb (negb (Nat.eqb ?x 0)) (andb (Nat.eqb ?x 0) ?y)) ]
               => let z := fresh in
                  let y' := fresh in
                  set (z := x);
                    set (y' := y);
                    refine (_ : orb (Compare_dec.leb 1 x) y = _);
-                   change (orb (Compare_dec.leb 1 z) y' = orb (negb (EqNat.beq_nat z 0)) (andb (EqNat.beq_nat z 0) y'));
+                   change (orb (Compare_dec.leb 1 z) y' = orb (negb (Nat.eqb z 0)) (andb (Nat.eqb z 0) y'));
                    destruct z, y'; reflexivity
             end. }
           apply (f_equal2 orb); fin_step_opt; [].
@@ -1749,7 +1749,7 @@ Section recursive_descent_parser.
     | [ |- context G[snd (of_string ?str')] ]
       => let G' := context G[opt.id (opt.snd (of_string str'))] in
          change G'
-    | [ |- context G[EqNat.beq_nat (opt2.id ?x) 0] ]
+    | [ |- context G[Nat.eqb (opt2.id ?x) 0] ]
       => let G' := context G[opt2.id (opt2.beq_nat x 0)] in
          change G'
     | [ |- context G[(opt2.id ?x, 0)] ]
@@ -1758,7 +1758,7 @@ Section recursive_descent_parser.
     | [ |- context G[(opt2.id ?x, opt2.id ?y)] ]
       => let G' := context G[opt2.id (x, y)] in
          change G'
-    | [ |- context G[EqNat.beq_nat (opt.id ?x) 0] ]
+    | [ |- context G[Nat.eqb (opt.id ?x) 0] ]
       => let G' := context G[opt.id (opt.beq_nat x 0)] in
          change G'
     | [ |- context G[S (opt2.id ?x)] ]
diff --git a/src/Parsers/ContextFreeGrammar/Carriers.v b/src/Parsers/ContextFreeGrammar/Carriers.v
index c06ae52dc..f73bbb4f5 100644
--- a/src/Parsers/ContextFreeGrammar/Carriers.v
+++ b/src/Parsers/ContextFreeGrammar/Carriers.v
@@ -106,7 +106,7 @@ Section grammar.
           { simpl.
             rewrite (string_lb eq_refl); trivial. }
           { simpl; intros H'.
-            specialize (IHxs idx (Le.le_S_n _ _ H')).
+            specialize (IHxs idx (proj2 (Nat.succ_le_mono _ _) H')).
             rewrite first_index_helper_first_index_error, IHxs by omega.
             apply first_index_error_Some_correct in IHxs.
             repeat match goal with
diff --git a/src/Parsers/ContextFreeGrammar/Properties.v b/src/Parsers/ContextFreeGrammar/Properties.v
index d82f34ab6..e28fe2688 100644
--- a/src/Parsers/ContextFreeGrammar/Properties.v
+++ b/src/Parsers/ContextFreeGrammar/Properties.v
@@ -1,5 +1,5 @@
 (** * Properties about Context Free Grammars *)
-Require Import Coq.Numbers.Natural.Peano.NPeano Coq.Lists.List.
+Require Import Coq.Lists.List Coq.Arith.PeanoNat.
 Require Import Fiat.Common Fiat.Common.UIP.
 Require Import Fiat.Parsers.ContextFreeGrammar.Core.
 Require Import Fiat.Parsers.ContextFreeGrammar.Equality.
diff --git a/src/Parsers/ContextFreeGrammar/ValidReflective.v b/src/Parsers/ContextFreeGrammar/ValidReflective.v
index 95d7f36a6..7cc16b397 100644
--- a/src/Parsers/ContextFreeGrammar/ValidReflective.v
+++ b/src/Parsers/ContextFreeGrammar/ValidReflective.v
@@ -59,7 +59,7 @@ Section cfg.
       | [ H : List.Forall _ (_::_) |- _ ] => inversion H; clear H
       | _ => progress subst
       | _ => congruence
-      | [ H : EqNat.beq_nat _ _ = true |- _ ] => apply EqNat.beq_nat_true in H
+      | [ H : Nat.eqb _ _ = true |- _ ] => apply Nat.eqb_true in H
       | [ H : Equality.string_beq _ _ = true |- _ ] => apply Equality.string_bl in H
       | [ H : or _ _ |- _ ] => destruct H
       | [ H : forall x, @?A x \/ @?B x -> _ |- _ ]
diff --git a/src/Parsers/GenericCorrectnessBaseTypes.v b/src/Parsers/GenericCorrectnessBaseTypes.v
index d209c8e18..59a7eb459 100644
--- a/src/Parsers/GenericCorrectnessBaseTypes.v
+++ b/src/Parsers/GenericCorrectnessBaseTypes.v
@@ -63,7 +63,7 @@ Section correctness.
       ret_Terminal_true_correct
       : forall str offset len ch,
           len = 0 \/ offset + len <= length str
-          -> (beq_nat len 1 && char_at_matches offset str ch)%bool = true
+          -> (Nat.eqb len 1 && char_at_matches offset str ch)%bool = true
           -> parse_item_is_correct
                (substring offset len str) (Terminal ch)
                true (ret_Terminal_true (unsafe_get offset str));
diff --git a/src/Parsers/GenericRecognizer.v b/src/Parsers/GenericRecognizer.v
index e9fd7a2ec..08561854d 100644
--- a/src/Parsers/GenericRecognizer.v
+++ b/src/Parsers/GenericRecognizer.v
@@ -6,7 +6,6 @@ Require Import Fiat.Parsers.ContextFreeGrammar.Core.
 Require Import Fiat.Parsers.BaseTypes.
 Require Import Fiat.Parsers.GenericBaseTypes.
 Require Import Fiat.Common.Wf.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 
 Set Implicit Arguments.
 Local Open Scope string_like_scope.
@@ -25,7 +24,7 @@ Section recursive_descent_parser.
                  (it : item Char)
       : parse_item_T
         := match it with
-             | Terminal P => if EqNat.beq_nat len 1 && char_at_matches offset str P
+             | Terminal P => if Nat.eqb len 1 && char_at_matches offset str P
                              then ret_Terminal_true (unsafe_get offset str)
                              else ret_Terminal_false (unsafe_get offset str)
              | NonTerminal nt => if is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt)
@@ -59,7 +58,7 @@ Section recursive_descent_parser.
                     parse_production_T)
                ((** 0-length production, only accept empty *)
                  fun _ offset len0_minus_len
-                 => if beq_nat (len0 - len0_minus_len) 0
+                 => if Nat.eqb (len0 - len0_minus_len) 0
                     then ret_production_nil_true
                     else ret_production_nil_false)
                (fun it its parse_production' idx offset len0_minus_len
@@ -117,12 +116,12 @@ Section recursive_descent_parser.
                                  (offset : nat) (len : nat),
                             len <= fst p -> nonterminal_carrierT -> parse_nt_T).
 
-          Lemma pred_lt_beq {x} : negb (beq_nat x 0) = true -> pred x < x.
+          Lemma pred_lt_beq {x} : negb (Nat.eqb x 0) = true -> pred x < x.
           Proof.
             destruct x; simpl; try congruence; try omega.
           Qed.
           Lemma pred_lt_beq_helper {valid nt x}
-            : (negb (beq_nat x 0) && is_valid_nonterminal valid nt)%bool = true -> pred x < x.
+            : (negb (Nat.eqb x 0) && is_valid_nonterminal valid nt)%bool = true -> pred x < x.
           Proof.
             intro is_valid.
             generalize (proj1 (proj1 (Bool.andb_true_iff _ _) is_valid)).
@@ -162,7 +161,7 @@ Section recursive_descent_parser.
                                   initial_nonterminals_data
                                   offset'
                                   (len - len0_minus_len')
-                                  (le_minus _ _)))
+                                  (Nat.le_sub_l _ _)))
                     (fun _ => (** [str] didn't get smaller, so we cache the fact that we've hit this nonterminal already *)
                        sumbool_rect
                          (fun _ => option (forall (offset' : nat) (len0_minus_len' : nat), nonterminal_carrierT -> parse_nt_T))
@@ -174,11 +173,11 @@ Section recursive_descent_parser.
                                        (remove_nonterminal valid nt)
                                        offset'
                                        (len0 - len0_minus_len')
-                                       (le_minus _ _)))
+                                       (Nat.le_sub_l _ _)))
 
                          (fun _ => (** oops, we already saw this nonterminal in the past.  ABORT! *)
                             None)
-                         (Sumbool.sumbool_of_bool (negb (EqNat.beq_nat valid_len 0) && is_valid_nonterminal valid nt)))
+                         (Sumbool.sumbool_of_bool (negb (Nat.eqb valid_len 0) && is_valid_nonterminal valid nt)))
                     (lt_dec len len0)));
               first [ assumption
                     | apply le_minus
diff --git a/src/Parsers/GenericRecognizerMin.v b/src/Parsers/GenericRecognizerMin.v
index 579837c1a..0c101ba1a 100644
--- a/src/Parsers/GenericRecognizerMin.v
+++ b/src/Parsers/GenericRecognizerMin.v
@@ -840,7 +840,7 @@ Section recursive_descent_parser.
           : dec (minimal_parse_of_item (G := G) len0 valid (substring offset (len0 - len0_minus_len) str) it).
           Proof.
             refine (match it return dec (minimal_parse_of_item len0 valid (substring offset _ str) it) with
-                      | Terminal P => if Sumbool.sumbool_of_bool (EqNat.beq_nat (len0 - len0_minus_len) 1 && char_at_matches offset str P)%bool
+                      | Terminal P => if Sumbool.sumbool_of_bool (Nat.eqb (len0 - len0_minus_len) 1 && char_at_matches offset str P)%bool
                                       then inl (match get offset str as g return get offset str = g -> _ with
                                                 | Some ch => fun H => MinParseTerminal _ _ _ ch _ _ _
                                                 | None => fun _ => !
@@ -1046,7 +1046,7 @@ Section recursive_descent_parser.
         Local Ltac parse_production'_for_t' :=
           idtac;
           match goal with
-            | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H
+            | [ H : (beq_nat _ _) = true |- _ ] => apply Nat.eqb_true in H
             | _ => progress subst
             | _ => solve [ constructor; assumption
                          | constructor;
@@ -1628,7 +1628,7 @@ Section recursive_descent_parser.
                         (fun _ => _)
                         (fun is_valid => _)
                         (fun is_valid => _)
-                        (Sumbool.sumbool_of_bool (negb (EqNat.beq_nat valid_len 0) && is_valid_nonterminal valid nt)));
+                        (Sumbool.sumbool_of_bool (negb (Nat.eqb valid_len 0) && is_valid_nonterminal valid nt)));
               [ ((** It was valid, so we can remove it *)
                   edestruct (fun pf'' pf'''
                             => @parse_productions'
diff --git a/src/Parsers/GenericRecognizerOptimized.v b/src/Parsers/GenericRecognizerOptimized.v
index 0727dae96..2114e7a3f 100644
--- a/src/Parsers/GenericRecognizerOptimized.v
+++ b/src/Parsers/GenericRecognizerOptimized.v
@@ -333,7 +333,7 @@ Section recursive_descent_parser.
                                               (fun _ => _)
                                               (N0 a' b' c')
                                               (list_rect P0 (fun _ _ _ => ret_production_nil_true) C0 ls' a' b' c')
-                                              (EqNat.beq_nat (List.length ls') 0))
+                                              (Nat.eqb (List.length ls') 0))
                                            = list_rect P0 N0 C0 ls' a' b' c')
                              _
                              _
@@ -360,7 +360,7 @@ Section recursive_descent_parser.
             end. }
           { simpl.
             match goal with
-            | [ |- context[EqNat.beq_nat (List.length ?ls) 0] ]
+            | [ |- context[Nat.eqb (List.length ?ls) 0] ]
               => is_var ls; destruct ls; simpl; try reflexivity
             end; [].
             repeat match goal with
@@ -422,7 +422,7 @@ Section recursive_descent_parser.
               { apply (f_equal3 (fun (b : bool) x y => if b then x else y)); [ | reflexivity | reflexivity ].
                 apply (f_equal2 andb); [ | reflexivity ].
                 match goal with
-                | [ |- _ = EqNat.beq_nat (min ?v ?x) ?v ]
+                | [ |- _ = Nat.eqb (min ?v ?x) ?v ]
                   => refine (_ : Compare_dec.leb v x = _)
                 end.
                 match goal with
@@ -592,8 +592,8 @@ Section recursive_descent_parser.
               => transitivity (if (orb (negb b') b) then t else f); [ | destruct b, b'; reflexivity ]
             end; fin_step_opt.
             match goal with
-            | [ |- context[negb (EqNat.beq_nat ?x 0)] ]
-              => replace (negb (EqNat.beq_nat x 0)) with (Compare_dec.leb 1 x)
+            | [ |- context[negb (Nat.eqb ?x 0)] ]
+              => replace (negb (Nat.eqb x 0)) with (Compare_dec.leb 1 x)
                 by (destruct x as [|[]]; reflexivity)
             end.
             reflexivity. }
@@ -615,8 +615,8 @@ Section recursive_descent_parser.
               => transitivity (if (orb (negb b') b) then t else f); [ | destruct b, b'; reflexivity ]
             end; fin_step_opt.
             match goal with
-            | [ |- context[negb (EqNat.beq_nat ?x 0)] ]
-              => replace (negb (EqNat.beq_nat x 0)) with (Compare_dec.leb 1 x)
+            | [ |- context[negb (Nat.eqb ?x 0)] ]
+              => replace (negb (Nat.eqb x 0)) with (Compare_dec.leb 1 x)
                 by (destruct x as [|[]]; reflexivity)
             end.
             reflexivity. }
diff --git a/src/Parsers/GenericRecognizerOptimizedTactics.v b/src/Parsers/GenericRecognizerOptimizedTactics.v
index 111104d2e..e021edd13 100644
--- a/src/Parsers/GenericRecognizerOptimizedTactics.v
+++ b/src/Parsers/GenericRecognizerOptimizedTactics.v
@@ -66,9 +66,9 @@ Ltac t_reduce_fix :=
          | [ H : (_ && _)%bool = true |- _ ] => apply Bool.andb_true_iff in H
          | [ H : _ = in_left |- _ ] => clear H
          | [ H : _ /\ _ |- _ ] => destruct H
-         | [ H : context[negb (EqNat.beq_nat ?x ?y)] |- _ ] => destruct (EqNat.beq_nat x y) eqn:?
-         | [ H : EqNat.beq_nat _ _ = false |- _ ] => apply EqNat.beq_nat_false in H
-         | [ H : EqNat.beq_nat _ _ = true |- _ ] => apply EqNat.beq_nat_true in H
+         | [ H : context[negb (Nat.eqb ?x ?y)] |- _ ] => destruct (Nat.eqb x y) eqn:?
+         | [ H : Nat.eqb _ _ = false |- _ ] => apply Nat.eqb_false in H
+         | [ H : Nat.eqb _ _ = true |- _ ] => apply Nat.eqb_true in H
          | [ H : snd ?x = _ |- _ ] => is_var x; destruct x
          | _ => progress simpl negb in *
          | [ H : false = true |- _ ] => inversion H
@@ -200,7 +200,7 @@ Ltac fin_step_opt :=
          | [ |- _ = 0 ] => reflexivity
          | [ |- _ = 1 ] => reflexivity
          | [ |- _ = None ] => reflexivity
-         | [ |- _ = EqNat.beq_nat _ _ ] => apply f_equal2
+         | [ |- _ = Nat.eqb _ _ ] => apply f_equal2
          | [ |- _ = Compare_dec.leb _ _ ] => apply f_equal2
          | [ |- _ = S _ ] => apply f_equal
          | [ |- _ = string_beq _ _ ] => apply f_equal2
diff --git a/src/Parsers/Reachable/ParenBalanced/Core.v b/src/Parsers/Reachable/ParenBalanced/Core.v
index f9d9c6858..3b03ff8a5 100644
--- a/src/Parsers/Reachable/ParenBalanced/Core.v
+++ b/src/Parsers/Reachable/ParenBalanced/Core.v
@@ -84,7 +84,7 @@ pb = pb' '+' 0
 
   Definition pb_new_level_fun (P : Char -> bool) (start_level : nat) : list nat
     := List.uniquize
-         EqNat.beq_nat
+         Nat.eqb
          (List.map
             (fun ch => pb_new_level ch start_level)
             (List.filter
@@ -96,7 +96,7 @@ pb = pb' '+' 0
     <-> ((exists ch, P ch) /\ forall ch, P ch -> new_level = pb_new_level ch start_level).
   Proof.
     unfold pb_new_level_fun.
-    rewrite (uniquize_singleton (beq := EqNat.beq_nat) bl lb).
+    rewrite (uniquize_singleton (beq := Nat.eqb) bl lb).
     setoid_rewrite in_map_iff.
     setoid_rewrite filter_In.
     setoid_rewrite (fun x => @and_TrueP_L (In x (enumerate Char)) (P x = true) (enumerate_correct _)).
diff --git a/src/Parsers/RecognizerPreOptimized.v b/src/Parsers/RecognizerPreOptimized.v
index 247f724a5..d83f82a5f 100644
--- a/src/Parsers/RecognizerPreOptimized.v
+++ b/src/Parsers/RecognizerPreOptimized.v
@@ -1,7 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Fiat.Parsers.ContextFreeGrammar.Core.
 Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations.
 Require Import Fiat.Parsers.BaseTypes.
diff --git a/src/Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar.v b/src/Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar.v
index 022d719b5..2cd802254 100644
--- a/src/Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar.v
+++ b/src/Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar.v
@@ -186,7 +186,7 @@ Section specific.
                        | [ H : forall x, _ = x -> _ |- _ ] => specialize (H _ eq_refl)
                        | [ H : forall x, x = _ -> _ |- _ ] => specialize (H _ eq_refl)
                        | [ H : context[In _ (uniquize _ _)] |- _ ]
-                         => setoid_rewrite <- (ListFacts.uniquize_In_refl_iff _ EqNat.beq_nat _ (lb eq_refl) bl) in H
+                         => setoid_rewrite <- (ListFacts.uniquize_In_refl_iff _ Nat.eqb _ (lb eq_refl) bl) in H
                        | [ H : context[In _ (map _ _)] |- _ ]
                          => setoid_rewrite in_map_iff in H
                        | _ => progress destruct_head ex
@@ -284,7 +284,7 @@ Section specific.
                  | _ => progress subst
                  | _ => congruence
                  | [ H : string_beq _ _ = true |- _ ] => apply string_bl in H
-                 | [ H : EqNat.beq_nat _ _ = true |- _ ] => apply EqNat.beq_nat_true in H
+                 | [ H : Nat.eqb _ _ = true |- _ ] => apply Nat.eqb_true in H
                  | [ H : is_true (_ || _) |- _ ] => apply Bool.orb_true_iff in H
                  | [ H : is_true (_ && _) |- _ ] => apply Bool.andb_true_iff in H
                  | [ H : _ /\ _ |- _ ] => let H1 := fresh in
diff --git a/src/Parsers/Refinement/DisjointLemmas.v b/src/Parsers/Refinement/DisjointLemmas.v
index a3e89efd7..3680e2072 100644
--- a/src/Parsers/Refinement/DisjointLemmas.v
+++ b/src/Parsers/Refinement/DisjointLemmas.v
@@ -3,7 +3,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Coq.Init.Wf Coq.Arith.Wf_nat.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Lists.List Coq.Strings.String.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Fiat.Parsers.ContextFreeGrammar.Core.
 Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations.
 Require Import Fiat.Parsers.ContextFreeGrammar.Equality.
diff --git a/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v b/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v
index b07518e6b..9b712f9c4 100644
--- a/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v
+++ b/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v
@@ -1,7 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** First step of a splitter refinement; indexed representation, and handle all rules with at most one nonterminal; leave a reflective goal *)
 Require Import Coq.Strings.String Coq.Arith.Lt Coq.Lists.List.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Fiat.Parsers.BaseTypes.
 Require Import Fiat.Parsers.Splitters.RDPList.
 Require Import Fiat.Parsers.ParserInterface.
@@ -237,10 +236,10 @@ Module Export PrettyNotations.
   Infix "=p" := default_production_carrierT_beq (at level 70, no associativity).
   Infix "=ℕ" := opt.beq_nat (at level 70, no associativity).
   Infix "=ℕ" := opt2.beq_nat (at level 70, no associativity).
-  Infix "=ℕ" := EqNat.beq_nat (at level 70, no associativity).
+  Infix "=ℕ" := Nat.eqb (at level 70, no associativity).
 End PrettyNotations.
 
-Definition beq_nat_opt := Eval compute in EqNat.beq_nat.
+Definition beq_nat_opt := Eval compute in Nat.eqb.
 Definition andb_opt := Eval compute in andb.
 
 Inductive ret_cases : Set :=
@@ -257,12 +256,12 @@ Local Ltac t_ret_cases :=
          | _ => intro
          | _ => progress subst
          | _ => congruence
-         | [ H : ?f ?x ?y = ?b |- _ ] => progress change (EqNat.beq_nat x y = b) in H
-         | [ |- ?f ?x ?y = ?b ] => progress change (EqNat.beq_nat x y = b)
+         | [ H : ?f ?x ?y = ?b |- _ ] => progress change (Nat.eqb x y = b) in H
+         | [ |- ?f ?x ?y = ?b ] => progress change (Nat.eqb x y = b)
          | [ H : ?f ?x ?y = ?b |- _ ] => progress change (andb x y = b) in H
          | [ |- ?f ?x ?y = ?b ] => progress change (andb x y = b)
-         | [ H : EqNat.beq_nat _ _ = true |- _ ] => apply EqNat.beq_nat_true in H
-         | [ |- EqNat.beq_nat _ _ = true ] => apply EqNat.beq_nat_true_iff
+         | [ H : Nat.eqb _ _ = true |- _ ] => apply Nat.eqb_true in H
+         | [ |- Nat.eqb _ _ = true ] => apply Nat.eqb_true_iff
          | [ H : andb _ _ = true |- _ ] => apply Bool.andb_true_iff in H
          | [ |- andb _ _ = true ] => apply Bool.andb_true_iff
          | [ H : and _ _ |- _ ] => destruct H
@@ -741,7 +740,7 @@ Section IndexedImpl.
     end.
   Local Ltac pre_fin := repeat pre_fin'.
 
-  Local Arguments EqNat.beq_nat : simpl never.
+  Local Arguments Nat.eqb : simpl never.
 
   Local Ltac do_Iterate_Ensemble_BoundedIndex_equiv :=
     eapply Iterate_Ensemble_BoundedIndex_equiv;
@@ -776,8 +775,8 @@ Section IndexedImpl.
       | [ H : context[unsafe_get] |- _ ] => erewrite unsafe_get_correct in H by eassumption
       | [ H : andb _ _ = true |- _ ] => apply Bool.andb_true_iff in H
       | [ H : andb _ _ = false |- _ ] => apply Bool.andb_false_iff in H
-      | [ H : EqNat.beq_nat _ _ = true |- _ ] => apply EqNat.beq_nat_true in H
-      | [ H : EqNat.beq_nat _ _ = false |- _ ] => apply EqNat.beq_nat_false in H
+      | [ H : Nat.eqb _ _ = true |- _ ] => apply Nat.eqb_true in H
+      | [ H : Nat.eqb _ _ = false |- _ ] => apply Nat.eqb_false in H
       | [ H : Compare_dec.leb _ _ = true |- _ ] => apply Compare_dec.leb_complete in H
       | [ H : Compare_dec.leb _ _ = false |- _ ] => apply Compare_dec.leb_complete_conv in H
       | [ H : context[?x - ?x] |- _ ] => rewrite Minus.minus_diag in H
diff --git a/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt.v b/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt.v
index 446833ae9..ea14bfa14 100644
--- a/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt.v
+++ b/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt.v
@@ -519,7 +519,7 @@ Section IndexedImpl_opt.
                | [ |- opt.minus _ _ = _ ] => apply f_equal2
                | [ |- opt.combine _ _ = _ ] => apply f_equal2
                | [ |- opt2.ret_cases_BoolDecR _ _ = _ ] => apply f_equal2
-               | [ |- EqNat.beq_nat _ _ = _ ] => apply f_equal2
+               | [ |- Nat.eqb _ _ = _ ] => apply f_equal2
                | [ |- opt.nth _ _ _ = _ ] => apply f_equal3
                | [ |- 0 = _ ] => reflexivity
                | [ |- opt.length (pregrammar_productions G) = _ ] => reflexivity
@@ -572,7 +572,7 @@ Section IndexedImpl_opt.
       change (snd d) with (Common.opt2.snd d);
       change (fst (Common.opt2.snd d)) with (Common.opt2.fst (Common.opt2.snd d));
       change (snd (Common.opt2.snd d)) with (Common.opt2.snd (Common.opt2.snd d)).
-      change EqNat.beq_nat with Common.opt2.beq_nat.
+      change Nat.eqb with Common.opt2.beq_nat.
       change andb with Common.opt2.andb.
       reflexivity.
     }
diff --git a/src/Parsers/Refinement/PreTactics.v b/src/Parsers/Refinement/PreTactics.v
index 6d49acc33..e5405bad1 100644
--- a/src/Parsers/Refinement/PreTactics.v
+++ b/src/Parsers/Refinement/PreTactics.v
@@ -123,14 +123,14 @@ Ltac solve_prod_beq :=
   repeat match goal with
            | [ |- context[true = false] ] => congruence
            | [ |- context[false = true] ] => congruence
-           | [ |- context[EqNat.beq_nat ?x ?y] ]
+           | [ |- context[Nat.eqb ?x ?y] ]
              => is_var x;
                let H := fresh in
-               destruct (EqNat.beq_nat x y) eqn:H;
-                 [ apply EqNat.beq_nat_true in H; subst x
+               destruct (Nat.eqb x y) eqn:H;
+                 [ apply Nat.eqb_true in H; subst x
                  | ];
                  simpl
-           | [ |- context[EqNat.beq_nat ?x ?y] ]
+           | [ |- context[Nat.eqb ?x ?y] ]
              => first [ is_var x; fail 1
                       | generalize x; intro ]
          end.
diff --git a/src/Parsers/Reflective/ParserSemantics.v b/src/Parsers/Reflective/ParserSemantics.v
index 1dac18bc9..50006ada7 100644
--- a/src/Parsers/Reflective/ParserSemantics.v
+++ b/src/Parsers/Reflective/ParserSemantics.v
@@ -35,7 +35,7 @@ Proof.
             (fun is_valid
              => _)
             (fun _ => None)
-            (Sumbool.sumbool_of_bool (negb (EqNat.beq_nat valid_len0 0) && is_valid_nonterminal valids nt))%bool).
+            (Sumbool.sumbool_of_bool (negb (Nat.eqb valid_len0 0) && is_valid_nonterminal valids nt))%bool).
   refine (Some
             (fun offset' len0_minus_len' =>
                parse_nt len0 (pred valid_len0)
diff --git a/src/Parsers/Reflective/PartialUnfold.v b/src/Parsers/Reflective/PartialUnfold.v
index a6262beff..d4b142fe8 100644
--- a/src/Parsers/Reflective/PartialUnfold.v
+++ b/src/Parsers/Reflective/PartialUnfold.v
@@ -135,7 +135,7 @@ Section normalization_by_evaluation.
        | Rbeq_nat
          => specific_meaning_apply2
               cnat cnat cbool (syntactify_bool _)
-              EqNat.beq_nat
+              Nat.eqb
        | Rmap A B
          => fun af
             => option_map (@syntactify_list _ _)
diff --git a/src/Parsers/Reflective/Reify.v b/src/Parsers/Reflective/Reify.v
index e25d1030b..07dd10765 100644
--- a/src/Parsers/Reflective/Reify.v
+++ b/src/Parsers/Reflective/Reify.v
@@ -185,7 +185,7 @@ Ltac reify_Term var term
                        | andbr => constr:(@Randbr)
                        | minusr => constr:(@Rminusr)
                        | Compare_dec.leb => constr:(@Rleb)
-                       | EqNat.beq_nat => constr:(@Rbeq_nat)
+                       | Nat.eqb => constr:(@Rbeq_nat)
                        | Equality.string_beq => constr:(@Rstring_beq)
                        | @Reflective.interp_RCharExpr _ _ => constr:(@Rinterp_RCharExpr_ascii)
                        end in
diff --git a/src/Parsers/Reflective/Semantics.v b/src/Parsers/Reflective/Semantics.v
index 197478e48..6ba082192 100644
--- a/src/Parsers/Reflective/Semantics.v
+++ b/src/Parsers/Reflective/Semantics.v
@@ -90,7 +90,7 @@ Definition interp_RLiteralTerm {T} (t : RLiteralTerm T) : interp_TypeCode T
           | Rpred => pred
           | Rplus => plus
           | Rleb => Compare_dec.leb
-          | Rbeq_nat => EqNat.beq_nat
+          | Rbeq_nat => Nat.eqb
           | Rstring_beq => Equality.string_beq
           | Rlength _ => @List.length _
           | Rbool_rect_nodep _ => @bool_rect_nodep _
diff --git a/src/Parsers/SimpleRecognizerCorrect.v b/src/Parsers/SimpleRecognizerCorrect.v
index 029bae677..0d4fafde0 100644
--- a/src/Parsers/SimpleRecognizerCorrect.v
+++ b/src/Parsers/SimpleRecognizerCorrect.v
@@ -56,7 +56,7 @@ Section convenience.
     | _ => progress simpl in *
     | _ => progress simpl_simple_parse_of_correct
     | [ |- exists p, Some ?x = Some p /\ _ ] => exists x
-    | [ H : ?x = 0 \/ _, H' : andb (EqNat.beq_nat ?x (S _)) _ = true |- _ ]
+    | [ H : ?x = 0 \/ _, H' : andb (Nat.eqb ?x (S _)) _ = true |- _ ]
       => destruct H
     | [ H : andb _ (char_at_matches _ _ _) = true |- _ ]
       => apply char_at_matches_is_char_no_ex in H; [ | assumption ]
diff --git a/src/Parsers/SplitterFromParserADT.v b/src/Parsers/SplitterFromParserADT.v
index 0589a0273..a1f1bb191 100644
--- a/src/Parsers/SplitterFromParserADT.v
+++ b/src/Parsers/SplitterFromParserADT.v
@@ -184,7 +184,7 @@ Section parser.
     prove_string_eq.
   Qed.
   Definition mis_char (ch : Ascii.ascii) (str : cRep (projT1 splitter_impl)) : bool
-    := (EqNat.beq_nat (mlength str) 1 && mchar_at_matches 0 (ascii_beq ch) str)%bool.
+    := (Nat.eqb (mlength str) 1 && mchar_at_matches 0 (ascii_beq ch) str)%bool.
   Global Arguments mis_char : simpl never.
   Definition mis_char_eq {arg st str} (H : AbsR (projT2 splitter_impl) str st)
   : mis_char arg st = is_char str arg.
@@ -197,8 +197,8 @@ Section parser.
       destruct H' as [H'0 H'1].
       rewrite H'0, H'1; simpl.
       rewrite ascii_lb; reflexivity. }
-    { destruct (EqNat.beq_nat (length str) 1) eqn:H'0; simpl; [ | reflexivity ].
-      apply EqNat.beq_nat_true in H'0.
+    { destruct (Nat.eqb (length str) 1) eqn:H'0; simpl; [ | reflexivity ].
+      apply Nat.eqb_true in H'0.
       destruct (get 0 str) as [ch|] eqn:H'1; simpl; [ | exfalso ].
       { destruct (ascii_beq arg ch) eqn:H''; [ | reflexivity ].
         apply ascii_bl in H''; subst.
diff --git a/src/Parsers/Splitters/RDPList.v b/src/Parsers/Splitters/RDPList.v
index b3b03c8ac..f5a5782d3 100644
--- a/src/Parsers/Splitters/RDPList.v
+++ b/src/Parsers/Splitters/RDPList.v
@@ -26,14 +26,14 @@ Section recursive_descent_parser_list.
   Notation rdp_list_production_carrierT := default_production_carrierT.
 
   Definition list_bin_eq
-    := Eval unfold list_bin in list_bin EqNat.beq_nat.
+    := Eval unfold list_bin in list_bin Nat.eqb.
 
   Definition rdp_list_is_valid_nonterminal : rdp_list_nonterminals_listT -> rdp_list_nonterminal_carrierT -> bool
     := fun ls nt => list_bin_eq nt ls.
 
   Local Ltac fix_list_bin_eq :=
     unfold rdp_list_is_valid_nonterminal;
-    change list_bin_eq with (list_bin EqNat.beq_nat) in *.
+    change list_bin_eq with (list_bin Nat.eqb) in *.
 
   Local Notation valid_nonterminals := (map fst (pregrammar_productions G)).
 
@@ -292,7 +292,7 @@ Section recursive_descent_parser_list.
     intros nt Hnt.
     apply Forall_map, Forall_forall; unfold compose; simpl; intros ? H.
     fix_list_bin_eq.
-    apply list_in_bl in Hnt; [ | exact (EqNat.beq_nat_true) ].
+    apply list_in_bl in Hnt; [ | exact (Nat.eqb_true) ].
     apply in_up_to_iff in Hnt.
     unfold default_production_carrier_valid; simpl.
     repeat (apply Bool.andb_true_iff; split); apply leb_iff.
@@ -337,7 +337,7 @@ Section recursive_descent_parser_list.
   Qed.
 
   Definition filter_out_eq nt ls
-    := Eval unfold filter_out in filter_out (EqNat.beq_nat nt) ls.
+    := Eval unfold filter_out in filter_out (Nat.eqb nt) ls.
 
   Definition rdp_list_remove_nonterminal : rdp_list_nonterminals_listT -> rdp_list_nonterminal_carrierT -> rdp_list_nonterminals_listT
     := fun ls nt =>
@@ -345,7 +345,7 @@ Section recursive_descent_parser_list.
 
   Local Ltac fix_filter_out_eq :=
     unfold rdp_list_remove_nonterminal;
-    change filter_out_eq with (fun nt ls => filter_out (EqNat.beq_nat nt) ls); cbv beta;
+    change filter_out_eq with (fun nt ls => filter_out (Nat.eqb nt) ls); cbv beta;
     setoid_rewrite filter_out_filter.
 
   Local Ltac fix_eqs := try fix_filter_out_eq; try fix_list_bin_eq.
diff --git a/src/Parsers/StringLike/FirstChar.v b/src/Parsers/StringLike/FirstChar.v
index 670465cda..d2385edb0 100644
--- a/src/Parsers/StringLike/FirstChar.v
+++ b/src/Parsers/StringLike/FirstChar.v
@@ -2,7 +2,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** * Mapping predicates over [StringLike] things *)
 
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Fiat.Parsers.StringLike.Core.
 Require Import Fiat.Parsers.StringLike.Properties.
 Require Import Fiat.Parsers.StringLike.ForallChars.
diff --git a/src/Parsers/StringLike/FirstCharSuchThat.v b/src/Parsers/StringLike/FirstCharSuchThat.v
index 29bfb322e..155381648 100644
--- a/src/Parsers/StringLike/FirstCharSuchThat.v
+++ b/src/Parsers/StringLike/FirstCharSuchThat.v
@@ -1,7 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** * Mapping predicates over [StringLike] things *)
 
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Fiat.Parsers.StringLike.Core.
 Require Import Fiat.Parsers.StringLike.Properties.
 Require Import Fiat.Parsers.StringLike.ForallChars.
diff --git a/src/Parsers/StringLike/ForallChars.v b/src/Parsers/StringLike/ForallChars.v
index cdb8395d3..412f53d9a 100644
--- a/src/Parsers/StringLike/ForallChars.v
+++ b/src/Parsers/StringLike/ForallChars.v
@@ -1,7 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** * Mapping predicates over [StringLike] things *)
 
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
 Require Import Fiat.Parsers.StringLike.Core.
 Require Import Fiat.Parsers.StringLike.Properties.
diff --git a/src/Parsers/StringLike/LastChar.v b/src/Parsers/StringLike/LastChar.v
index bb5a60467..6f3c94a6f 100644
--- a/src/Parsers/StringLike/LastChar.v
+++ b/src/Parsers/StringLike/LastChar.v
@@ -1,7 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** * Mapping predicates over [StringLike] things *)
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Fiat.Parsers.StringLike.Core.
 Require Import Fiat.Parsers.StringLike.Properties.
 Require Import Fiat.Parsers.StringLike.ForallChars.
diff --git a/src/Parsers/StringLike/LastCharSuchThat.v b/src/Parsers/StringLike/LastCharSuchThat.v
index 33b515e3d..270f7da2f 100644
--- a/src/Parsers/StringLike/LastCharSuchThat.v
+++ b/src/Parsers/StringLike/LastCharSuchThat.v
@@ -1,7 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** * Mapping predicates over [StringLike] things *)
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Fiat.Parsers.StringLike.Core.
 Require Import Fiat.Parsers.StringLike.Properties.
 Require Import Fiat.Parsers.StringLike.ForallChars.
diff --git a/src/Parsers/StringLike/OcamlString.v b/src/Parsers/StringLike/OcamlString.v
index 66129921a..83e6a13f3 100644
--- a/src/Parsers/StringLike/OcamlString.v
+++ b/src/Parsers/StringLike/OcamlString.v
@@ -1,5 +1,4 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
@@ -38,19 +37,19 @@ Local Ltac t' :=
     | _ => exfalso; congruence
     | _ => rewrite substring_length
     | _ => rewrite <- plus_n_O
-    | _ => rewrite <- Minus.minus_n_O
-    | _ => rewrite Min.min_l by omega
-    | _ => rewrite Min.min_r by omega
+    | _ => rewrite Nat.sub_0_r
+    | _ => rewrite Nat.min_l by omega
+    | _ => rewrite Nat.min_r by omega
     | _ => rewrite substring_correct3 by assumption
     | _ => rewrite substring_substring
     | _ => rewrite substring_correct3'
     | _ => rewrite substring_correct0
     | _ => rewrite Nat.sub_min_distr_l
     | _ => rewrite Nat.add_sub
-    | _ => rewrite Min.min_0_r
-    | _ => rewrite Min.min_0_l
+    | _ => rewrite Nat.min_0_r
+    | _ => rewrite Nat.min_0_l
     | _ => rewrite Nat.add_1_r
-    | _ => rewrite <- Min.min_assoc
+    | _ => rewrite <- Nat.min_assoc
     | [ |- String.get _ _ = _ ] => apply StringProperties.get_correct
     | _ => progress rewrite ?string_beq_correct, ?ascii_beq_correct, ?string_copy_length
     | [ H : _ |- _ ] => progress rewrite ?string_beq_correct, ?ascii_beq_correct in H
@@ -59,11 +58,11 @@ Local Ltac t' :=
         by (rewrite <- Nat.sub_min_distr_l; apply f_equal2; omega)
     | [ |- context[min (?m + ?n) ?m] ]
       => replace (min (m + n) m) with (m + min n 0)
-        by (rewrite <- Min.plus_min_distr_l; apply f_equal2; omega)
-    | _ => rewrite Min.min_comm; reflexivity
+        by (rewrite <- Nat.add_min_distr_l; apply f_equal2; omega)
+    | _ => rewrite Nat.min_comm; reflexivity
     | [ |- context[string_eq_dec ?x ?y] ] => destruct (string_eq_dec x y)
     | [ H : _ <> _ |- False ] => apply H; clear H
-    | _ => apply Max.max_case_strong; intro; apply substring_correct4; omega
+    | _ => apply Nat.max_case_strong; intro; apply substring_correct4; omega
     | [ H : Coq.Strings.String.length ?s = 1 |- _ ] => is_var s; destruct s
     | [ H : S (Coq.Strings.String.length ?s) = 1 |- _ ] => is_var s; destruct s
     | _ => eexists; rewrite (ascii_lb eq_refl); reflexivity
@@ -77,9 +76,9 @@ Local Ltac t' :=
         | rewrite substring_correct2 by omega ]
     | _ => rewrite <- substring_correct3'; apply substring_correct2; omega
     | [ H : forall n, Coq.Strings.String.get n _ = Coq.Strings.String.get n _ |- _ ] => apply get_correct in H
-    | [ H : EqNat.beq_nat _ _ = true |- _ ] => apply EqNat.beq_nat_true in H
-    | [ H : EqNat.beq_nat _ _ = false |- _ ] => apply EqNat.beq_nat_false in H
-    | [ H : context[EqNat.beq_nat ?x ?y] |- _ ] => destruct (EqNat.beq_nat x y) eqn:?
+    | [ H : Nat.eqb _ _ = true |- _ ] => apply (proj1 (Nat.eqb_eq _ _)) in H
+    | [ H : Nat.eqb _ _ = false |- _ ] => apply (proj1 (Nat.eqb_neq _ _)) in H
+    | [ H : context[Nat.eqb ?x ?y] |- _ ] => destruct (Nat.eqb x y) eqn:?
     | [ H : context[option_beq ascii_beq _ _] |- _ ] => rewrite (option_beq_correct (@ascii_bl) (@ascii_lb)) in H
     | [ H : context[option_eq_dec ?beq ?bl ?lb ?x ?y] |- _ ] => destruct (option_eq_dec beq bl lb x y)
     | _ => progress change (andb true) with (fun x : bool => x) in *
@@ -107,7 +106,7 @@ Local Ltac t' :=
     | [ |- String.substring ?n ?m ?s = String.substring ?n ?m' ?s ]
       => not constr_eq m m'; replace m with m' by omega
     | [ |- String.substring ?n ?m ?s = String.substring ?n ?m' ?s ]
-      => not constr_eq m m'; replace m with m' by (repeat apply Min.min_case_strong; intros; omega)
+      => not constr_eq m m'; replace m with m' by (repeat apply Nat.min_case_strong; intros; omega)
   end.
 
 Local Ltac t := repeat t'.
@@ -123,7 +122,7 @@ Module Export Ocaml.
     := { get n s := String.safe_get s n;
          take n s := String.sub s 0 n;
          drop n s := String.sub s n (String.length s - n);
-         is_char s ch := ((EqNat.beq_nat (String.length s) 1)
+         is_char s ch := ((Nat.eqb (String.length s) 1)
                             && (option_beq ascii_beq (String.safe_get s 0) (Some ch)))%bool;
          bool_eq s1 s2 := Zbool.Zeq_bool (z_of_int (Ocaml.String.compare s1 s2)) 0%Z }.
 
diff --git a/src/Parsers/StringLike/Properties.v b/src/Parsers/StringLike/Properties.v
index ff95f9929..56bd38370 100644
--- a/src/Parsers/StringLike/Properties.v
+++ b/src/Parsers/StringLike/Properties.v
@@ -1,7 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** * Theorems about string-like types *)
 
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
 Require Import Fiat.Common.
 Require Import Fiat.Common.List.Operations.
@@ -147,10 +146,10 @@ Section String.
   Proof.
     destruct (le_ge_dec (length str) n).
     { rewrite take_long by assumption.
-      rewrite Min.min_r by assumption.
+      rewrite Nat.min_r by assumption.
       reflexivity. }
     { rewrite take_short_length by assumption.
-      rewrite Min.min_l by assumption.
+      rewrite Nat.min_l by assumption.
       reflexivity. }
   Qed.
 
@@ -188,14 +187,14 @@ Section String.
       destruct H0' as [H''|H'']; try clear H0'; [ apply f_equal | exfalso ].
       { apply le_proof_irrelevance. }
       { setoid_subst s1.
-        eapply lt_irrefl; eassumption. }
+        eapply Nat.lt_irrefl; eassumption. }
     Qed.
 
     Definition strle_right (H' : s1 =s s2)
     : H0' = or_intror H'.
     Proof.
       destruct H0' as [H''|H'']; try clear H0'; [ exfalso | apply f_equal ].
-      { setoid_subst s1; eapply lt_irrefl; eassumption. }
+      { setoid_subst s1; eapply Nat.lt_irrefl; eassumption. }
       { apply dec_eq_uip.
         decide equality. }
     Qed.
@@ -208,7 +207,7 @@ Section String.
   : False.
   Proof.
     rewrite H' in H0'.
-    eapply lt_irrefl; eassumption.
+    eapply Nat.lt_irrefl; eassumption.
   Qed.
 
   Lemma singleton_exists_unique : forall s, length s = 1 -> exists !ch, s ~= [ ch ].
@@ -236,7 +235,7 @@ Section String.
   Lemma take_empty {str n} (H' : length str = 0) : take n str =s str.
   Proof.
     apply bool_eq_empty; rewrite ?drop_length, ?take_length; trivial.
-    apply Min.min_case_strong; omega.
+    apply Nat.min_case_strong; omega.
   Qed.
 
   Definition get_first_char_nonempty' str (H' : length str <> 0) : Char.
@@ -380,7 +379,7 @@ Section String.
     { intros.
       rewrite !(@get_drop (length _ - _)).
       rewrite drop_length, drop_drop.
-      rewrite <- Nat.sub_add_distr, (plus_comm m), Nat.sub_add_distr, Nat.sub_add by omega.
+      rewrite <- Nat.sub_add_distr, (Nat.add_comm m), Nat.sub_add_distr, Nat.sub_add by omega.
       match goal with
         | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:?
       end.
@@ -413,9 +412,9 @@ Section String.
         congruence. }
       { intros ? H''.
         rewrite fold'_cons.
-        rewrite !H'', minus_diag, H'.
+        rewrite !H'', Nat.sub_diag, H'.
         rewrite drop_length, H''; simpl.
-        rewrite <- minus_n_O.
+        rewrite Nat.sub_0_r.
         apply f_equal.
         rewrite <- fold'_drop by omega; reflexivity. } }
     { intro H'.
@@ -475,12 +474,12 @@ Section String.
     { intros.
       rewrite !(@get_drop (length _ - _)).
       rewrite drop_length, drop_drop.
-      rewrite <- Nat.sub_add_distr, (plus_comm m), Nat.sub_add_distr, Nat.sub_add by omega.
+      rewrite <- Nat.sub_add_distr, (Nat.add_comm m), Nat.sub_add_distr, Nat.sub_add by omega.
       match goal with
         | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:?
       end.
       { rewrite drop_drop;
-        rewrite <- Nat.sub_add_distr, (plus_comm m), Nat.sub_add_distr, Nat.sub_add by omega;
+        rewrite <- Nat.sub_add_distr, (Nat.add_comm m), Nat.sub_add_distr, Nat.sub_add by omega;
         rewrite <- IHlen by omega; reflexivity. }
       { reflexivity. } }
   Qed.
@@ -510,10 +509,10 @@ Section String.
         congruence. }
       { intros n H''.
         rewrite fold_lookahead'_cons.
-        rewrite !H'', minus_diag, H'.
+        rewrite !H'', Nat.sub_diag, H'.
         replace (S n - n) with 1 by omega.
         rewrite drop_length, H''; simpl.
-        rewrite <- minus_n_O.
+        rewrite Nat.sub_0_r.
         apply f_equal.
         rewrite <- fold_lookahead'_drop by omega; reflexivity. } }
     { intro H'.
@@ -565,14 +564,14 @@ Section String.
              | [ H : length ?str = 0, H' : is_true (take _ ?str ~= [ _ ]) |- _ ]
                => apply length_singleton in H'
              | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H'
-             | [ H : context[min _ _] |- _ ] => revert H; apply Min.min_case_strong; intros
+             | [ H : context[min _ _] |- _ ] => revert H; apply Nat.min_case_strong; intros
            end.
   Qed.
 
   Lemma take_min_length (str : String) n
   : take n str =s take (min (length str) n) str.
   Proof.
-    apply Min.min_case_strong; [ | reflexivity ].
+    apply Nat.min_case_strong; [ | reflexivity ].
     intro H.
     rewrite !take_long by (assumption || reflexivity).
     reflexivity.
@@ -581,7 +580,7 @@ Section String.
   Lemma drop_min_length (str : String) n
   : drop n str =s drop (min (length str) n) str.
   Proof.
-    apply Min.min_case_strong; [ | reflexivity ].
+    apply Nat.min_case_strong; [ | reflexivity ].
     intro H.
     apply bool_eq_empty; rewrite drop_length; omega.
   Qed.
@@ -626,7 +625,7 @@ Section String.
       | specialize (IHlen (drop 1 str));
         rewrite drop_length in IHlen;
         specialize_by omega;
-        try rewrite <- !H, !minus_diag;
+        try rewrite <- !H, !Nat.sub_diag;
         try rewrite <- fold'_drop in IHlen by omega ].
 
   Lemma to_string_length str
@@ -658,7 +657,7 @@ Section String.
              | [ |- context[length (take _ _)] ] => rewrite take_length
              | [ |- context[_ - 0] ] => rewrite Nat.sub_0_r
              | [ H : context[_ - 0] |- _ ] => rewrite Nat.sub_0_r in H
-             | [ |- context[fold' _ _ (drop _ _) _] ] => rewrite <- fold'_drop by (rewrite ?take_length; try apply Min.min_case_strong; omega)
+             | [ |- context[fold' _ _ (drop _ _) _] ] => rewrite <- fold'_drop by (rewrite ?take_length; try apply Nat.min_case_strong; omega)
              | [ H : context[fold' _ _ (drop _ _) _] |- _ ] => rewrite <- fold'_drop in H by omega
              | [ H : ?x = ?y |- context[?x - ?y] ] => replace (x - y) with 0 by omega
              | [ H : ?y = ?x |- context[?x - ?y] ] => replace (x - y) with 0 by omega
@@ -672,12 +671,12 @@ Section String.
              | [ |- context[?x + 1] ] => rewrite Nat.add_1_r
              | [ H : S _ = ?x |- context[match ?x with _ => _ end] ] => rewrite <- H
              | [ H : S _ = ?x, H' : context[match ?x with _ => _ end] |- _ ] => rewrite <- H in H'
-             | [ H : context[?x - ?x] |- _ ] => rewrite minus_diag in H
-             | [ |- context[?x - ?x] ] => rewrite minus_diag
+             | [ H : context[?x - ?x] |- _ ] => rewrite Nat.sub_diag in H
+             | [ |- context[?x - ?x] ] => rewrite Nat.sub_diag
              | [ H : context[get _ (take _ _)] |- _ ] => rewrite get_take_lt in H by omega
-             | [ H : context[min (pred ?x) ?x] |- _ ] => rewrite (Min.min_l (pred x) x) in H by omega
+             | [ H : context[min (pred ?x) ?x] |- _ ] => rewrite (Nat.min_l (pred x) x) in H by omega
              | [ |- context[take _ (drop _ _)] ] => rewrite take_drop
-             | [ |- context[min ?x ?y] ] => rewrite (Min.min_l x y) by omega
+             | [ |- context[min ?x ?y] ] => rewrite (Nat.min_l x y) by omega
              | [ |- context[get _ (drop 0 ?s)] ] => rewrite (drop_0 s)
              | [ |- context[get _ (drop _ (drop _ _))] ] => rewrite drop_drop
              | [ H : S ?x = ?y, H' : S ?z = ?y |- _ ]
@@ -773,9 +772,9 @@ Section String.
         | [ |- context[min ?x ?y] ]
           => match goal with
                | [ |- context[min y x] ]
-                 => rewrite (Min.min_comm x y)
+                 => rewrite (Nat.min_comm x y)
              end
-        | _ => repeat apply Min.min_case_strong; omega
+        | _ => repeat apply Nat.min_case_strong; omega
       end.
 
     Local Ltac substring_t := repeat substring_t'.
@@ -824,14 +823,14 @@ Section String.
     Proof.
       pose proof (fun y x => @substring_substring str 0 z x y) as H'; simpl in *.
       setoid_rewrite Nat.sub_0_r in H'.
-      setoid_rewrite Min.min_comm in H'.
+      setoid_rewrite Nat.min_comm in H'.
       rewrite <- !H', H; reflexivity.
     Qed.
 
     Lemma substring_min_length str x y
     : substring x (min y (length str)) str =s substring x y str.
     Proof.
-      apply Min.min_case_strong; try reflexivity.
+      apply Nat.min_case_strong; try reflexivity.
       intro H.
       apply substring_correct4; omega.
     Qed.
@@ -840,16 +839,16 @@ Section String.
     : length (substring offset len s) = len.
     Proof.
       rewrite substring_length; destruct Hshort as [Hshort|Hshort];
-      try rewrite Min.min_r by (clear -Hshort; omega);
+      try rewrite Nat.min_r by (clear -Hshort; omega);
       subst; simpl;
-      rewrite <- ?NPeano.Nat.sub_min_distr_r, ?NPeano.Nat.add_sub, ?minus_diag, ?Min.min_0_r;
+      rewrite <- ?Nat.sub_min_distr_r, ?Nat.add_sub, ?Nat.sub_diag, ?Nat.min_0_r;
       reflexivity.
     Qed.
   End substring.
 
   Lemma char_at_matches_is_char_no_ex offset len str P
         (Hlen : offset + len <= length str)
-  : (EqNat.beq_nat len 1 && char_at_matches offset str P)%bool = true
+  : (Nat.eqb len 1 && char_at_matches offset str P)%bool = true
     <-> match get offset str with
           | Some ch => (P ch /\ substring offset len str ~= [ch])%string_like
           | None => False
@@ -859,7 +858,7 @@ Section String.
     { split; intro H.
       { apply Bool.andb_true_iff in H.
         destruct H as [H0 H1].
-        apply EqNat.beq_nat_true in H0; subst.
+        apply Nat.eqb_eq in H0; subst.
         erewrite char_at_matches_correct in H1 by eassumption.
         split; try assumption.
         rewrite get_drop in Heq.
@@ -871,22 +870,22 @@ Section String.
         apply Bool.andb_true_iff; split; [ | eassumption ].
         apply length_singleton in H1.
         rewrite substring_length, <- Nat.sub_min_distr_r, Nat.add_sub in H1.
-        apply EqNat.beq_nat_true_iff.
+        apply Nat.eqb_eq.
         revert H1.
-        apply Min.min_case_strong; intros; omega. } }
+        apply Nat.min_case_strong; intros; omega. } }
     { split; [ intro H | intros [] ].
       rewrite get_drop in Heq.
       apply no_first_char_empty in Heq.
       rewrite drop_length in Heq.
       apply Bool.andb_true_iff in H.
       destruct H as [H0 H1].
-      apply EqNat.beq_nat_true in H0; subst.
+      apply Nat.eqb_eq in H0; subst.
       omega. }
   Qed.
 
   Lemma char_at_matches_is_char offset len str P
         (Hlen : offset + len <= length str)
-  : (EqNat.beq_nat len 1 && char_at_matches offset str P)%bool = true
+  : (Nat.eqb len 1 && char_at_matches offset str P)%bool = true
     <-> (exists ch, P ch /\ substring offset len str ~= [ch])%string_like.
   Proof.
     rewrite char_at_matches_is_char_no_ex by assumption.
@@ -907,7 +906,7 @@ Section String.
       rewrite drop_length in Heq.
       apply length_singleton in H1.
       assert (len = 0) by omega; subst.
-      rewrite substring_length, <- Nat.sub_min_distr_r, Nat.add_sub, Min.min_0_r in H1.
+      rewrite substring_length, <- Nat.sub_min_distr_r, Nat.add_sub, Nat.min_0_r in H1.
       omega. }
   Qed.
 
@@ -970,7 +969,7 @@ Section Iso.
                end. }
       { intro n'; rewrite !get_S.
         rewrite drop_take, !drop_of_string; simpl.
-        rewrite NPeano.Nat.sub_0_r.
+        rewrite Nat.sub_0_r.
         destruct str; simpl;
         rewrite !IHn; simpl; trivial.
         destruct n; reflexivity. } }
@@ -1098,8 +1097,8 @@ Ltac simpl_string_like_no_setoid_step :=
   | [ H : @length ?Char ?HSLM ?str = @length ?Char ?HSLM ?str' |- _ ]
     => first [ generalize dependent (@length Char HSLM str'); intros; subst; clear str'
              | generalize dependent (@length Char HSLM str); intros; subst; clear str ]
-  | [ H : _ |- _ ] => progress rewrite ?take_length, ?drop_length, ?Min.min_0_r, ?Min.min_0_l, ?Nat.sub_0_l in H
-  | _ => progress rewrite ?take_length, ?drop_length, ?Min.min_0_r, ?Min.min_0_l, ?Nat.sub_0_l
+  | [ H : _ |- _ ] => progress rewrite ?take_length, ?drop_length, ?Nat.min_0_r, ?Nat.min_0_l, ?Nat.sub_0_l in H
+  | _ => progress rewrite ?take_length, ?drop_length, ?Nat.min_0_r, ?Nat.min_0_l, ?Nat.sub_0_l
   end.
 Ltac simpl_string_like_step :=
   first [ progress simpl_string_like_no_setoid_step
diff --git a/src/Parsers/StringLike/String.v b/src/Parsers/StringLike/String.v
index 83cfb16bc..f4cf71e53 100644
--- a/src/Parsers/StringLike/String.v
+++ b/src/Parsers/StringLike/String.v
@@ -3,7 +3,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import Coq.Arith.PeanoNat.
 Require Import Fiat.Common Fiat.Common.Equality.
 Require Import Fiat.Common.StringOperations Fiat.Common.StringFacts.
 Require Import Fiat.Parsers.StringLike.Core.
@@ -61,19 +61,19 @@ Local Ltac t :=
            | _ => exfalso; congruence
            | _ => rewrite substring_length
            | _ => rewrite <- plus_n_O
-           | _ => rewrite <- Minus.minus_n_O
-           | _ => rewrite Min.min_l by omega
-           | _ => rewrite Min.min_r by omega
+           | _ => rewrite Nat.sub_0_r
+           | _ => rewrite Nat.min_l by omega
+           | _ => rewrite Nat.min_r by omega
            | _ => rewrite substring_correct3 by assumption
            | _ => rewrite substring_substring
            | _ => rewrite substring_correct3'
            | _ => rewrite substring_correct0
            | _ => rewrite Nat.sub_min_distr_l
            | _ => rewrite Nat.add_sub
-           | _ => rewrite Min.min_0_r
-           | _ => rewrite Min.min_0_l
+           | _ => rewrite Nat.min_0_r
+           | _ => rewrite Nat.min_0_l
            | _ => rewrite Nat.add_1_r
-           | _ => rewrite <- Min.min_assoc
+           | _ => rewrite <- Nat.min_assoc
            | [ H : ?x = Some _ |- context[match ?x with _ => _ end] ] => rewrite H
            | _ => progress rewrite ?string_beq_correct, ?ascii_beq_correct, ?string_copy_length
            | [ H : _ |- _ ] => progress rewrite ?string_beq_correct, ?ascii_beq_correct in H
@@ -82,11 +82,11 @@ Local Ltac t :=
                by (rewrite <- Nat.sub_min_distr_l; apply f_equal2; omega)
            | [ |- context[min (?m + ?n) ?m] ]
              => replace (min (m + n) m) with (m + min n 0)
-               by (rewrite <- Min.plus_min_distr_l; apply f_equal2; omega)
-           | _ => rewrite Min.min_comm; reflexivity
+               by (rewrite <- Nat.add_min_distr_l; apply f_equal2; omega)
+           | _ => rewrite Nat.min_comm; reflexivity
            | [ |- context[string_eq_dec ?x ?y] ] => destruct (string_eq_dec x y)
            | [ H : _ <> _ |- False ] => apply H; clear H
-           | _ => apply Max.max_case_strong; intro; apply substring_correct4; omega
+           | _ => apply Nat.max_case_strong; intro; apply substring_correct4; omega
            | [ H : String.length ?s = 1 |- _ ] => is_var s; destruct s
            | [ H : S (String.length ?s) = 1 |- _ ] => is_var s; destruct s
            | _ => eexists; rewrite (ascii_lb eq_refl); reflexivity
@@ -124,7 +124,7 @@ Lemma substring_take_drop (str : String) n m
 Proof.
   simpl.
   rewrite substring_substring; simpl.
-  apply Min.min_case_strong; simpl; trivial; [].
+  apply Nat.min_case_strong; simpl; trivial; [].
   intro H.
   apply substring_correct4; omega.
 Qed.
diff --git a/src/QueryStructure/Implementation/Constraints/ConstraintChecksRefinements.v b/src/QueryStructure/Implementation/Constraints/ConstraintChecksRefinements.v
index 94f6f4572..3a41df4ff 100644
--- a/src/QueryStructure/Implementation/Constraints/ConstraintChecksRefinements.v
+++ b/src/QueryStructure/Implementation/Constraints/ConstraintChecksRefinements.v
@@ -819,7 +819,7 @@ Lemma refine_constraint_check_into_QueryResultComp :
                               (R tup2 /\ P' tup2))))
          (Bind
             (Count (For (QueryResultComp R (fun tup => Where (P tup) Return tup))))
-            (fun count => ret (negb (beq_nat count 0)))).
+            (fun count => ret (negb (Nat.eqb count 0)))).
 Proof.
   Local Transparent Count.
   unfold refine, Count, UnConstrQuery_In;
@@ -853,7 +853,7 @@ Lemma refine_constraint_check_into_query' :
                               (GetUnConstrRelation c tbl tup2 /\ P' tup2))))
          (Bind
             (Count (For (UnConstrQuery_In c tbl (fun tup => Where (P tup) Return tup))))
-            (fun count => ret (negb (beq_nat count 0)))).
+            (fun count => ret (negb (Nat.eqb count 0)))).
 Proof.
   intros; rewrite refine_constraint_check_into_QueryResultComp; eauto.
   reflexivity.
@@ -869,7 +869,7 @@ Corollary refine_constraint_check_into_query :
                            (GetUnConstrRelation c tbl tup2 /\ P (indexedRawTuple tup2)))))
       (Bind
          (Count (For (UnConstrQuery_In c tbl (fun tup => Where (P tup) Return tup))))
-         (fun count => ret (negb (beq_nat count 0)))).
+         (fun count => ret (negb (Nat.eqb count 0)))).
 Proof.
   intros.
   setoid_rewrite refine_constraint_check_into_query'; eauto.
@@ -888,7 +888,7 @@ Lemma refine_constraint_check_into_query'' :
                               (R tup2 /\ P' tup2))))
          (Bind
             (Count (For (QueryResultComp R (fun tup => Where (P tup) Return tup))))
-            (fun count => ret (negb (beq_nat count 0)))).
+            (fun count => ret (negb (Nat.eqb count 0)))).
 Proof.
   Local Transparent Count.
   unfold refine, Count, UnConstrQuery_In;
@@ -942,7 +942,7 @@ Lemma refine_functional_dependency_check_into_query :
                                         Where (tupleAgree_computational ref tup args1 /\
                                                ~ tupleAgree_computational ref tup args2)
                                               Return tup)))
-            (fun count => ret (beq_nat count 0))).
+            (fun count => ret (Nat.eqb count 0))).
 Proof.
   intros * is_dec ** .
 
@@ -994,7 +994,7 @@ Lemma refine_functional_dependency_check_into_query' :
                                         Where (tupleAgree_computational tup ref args1 /\
                                                ~ tupleAgree_computational tup ref args2)
                                               Return tup)))
-            (fun count => ret (beq_nat count 0))).
+            (fun count => ret (Nat.eqb count 0))).
 Proof.
   intros * is_dec ** .
 
@@ -1122,7 +1122,7 @@ Lemma refine_uniqueness_check_into_query' :
                                         Where (GetAttributeRaw tup attr
                                                = GetAttributeRaw tup' attr)
                                               Return tup')));
-            (ret (beq_nat c 0))).
+            (ret (Nat.eqb c 0))).
 Proof.
   intros.
   setoid_replace (forall tup', GetUnConstrRelation c idx tup' ->
diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/BagsProperties.v b/src/QueryStructure/Implementation/DataStructures/Bags/BagsProperties.v
index fa07743a0..909a28a83 100644
--- a/src/QueryStructure/Implementation/DataStructures/Bags/BagsProperties.v
+++ b/src/QueryStructure/Implementation/DataStructures/Bags/BagsProperties.v
@@ -65,7 +65,7 @@ Section BagsProperties.
   Proof.
     unfold _BagInsertCount, _bcount; intros;
     rewrite binsert_enumerate; simpl; destruct (bfind_matcher search_term item); simpl; eauto.
-    rewrite plus_comm; reflexivity.
+    rewrite Nat.add_comm; reflexivity.
   Qed.
 
 End BagsProperties.
diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/CountingListBags.v b/src/QueryStructure/Implementation/DataStructures/Bags/CountingListBags.v
index 0d9bdb835..2f65d8eed 100644
--- a/src/QueryStructure/Implementation/DataStructures/Bags/CountingListBags.v
+++ b/src/QueryStructure/Implementation/DataStructures/Bags/CountingListBags.v
@@ -213,7 +213,7 @@ Section CountingListBags.
     + trivial.
     + simpl; destruct (search_term a);
       simpl; rewrite <- IHcontainer; simpl; eauto.
-      rewrite (plus_comm 1); eauto using plus_assoc.
+      rewrite (Nat.add_comm 1); eauto using Nat.add_assoc.
   Qed.
 
   Lemma CountingList_BagCountCorrect :
@@ -222,7 +222,7 @@ Section CountingListBags.
     unfold BagCountCorrect, CountingListAsBag_bcount, CountingListAsBag_bfind,
     CountingList_RepInv; intros;
     pose proof (CountingList_BagCountCorrect_aux (ccontents container) search_term 0) as temp;
-    rewrite plus_0_r in temp; simpl in temp.
+    rewrite Nat.add_0_r in temp; simpl in temp.
     simpl; [ apply temp ].
   Qed.
 
diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/ListBags.v b/src/QueryStructure/Implementation/DataStructures/Bags/ListBags.v
index 2e8b9ca80..44654cd65 100644
--- a/src/QueryStructure/Implementation/DataStructures/Bags/ListBags.v
+++ b/src/QueryStructure/Implementation/DataStructures/Bags/ListBags.v
@@ -84,7 +84,7 @@ Section ListBags.
   Proof.
     unfold BagCountCorrect, ListAsBag_bcount, ListAsBag_bfind; intros;
     pose proof (List_BagCountCorrect_aux container search_term 0) as temp;
-    rewrite plus_0_r in temp; simpl in temp; exact temp.
+    rewrite Nat.add_0_r in temp; simpl in temp; exact temp.
   Qed.
 
   Lemma List_BagDeleteCorrect :
diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/RangeTreeBags.v b/src/QueryStructure/Implementation/DataStructures/Bags/RangeTreeBags.v
index fbd43c797..4b0feba8f 100644
--- a/src/QueryStructure/Implementation/DataStructures/Bags/RangeTreeBags.v
+++ b/src/QueryStructure/Implementation/DataStructures/Bags/RangeTreeBags.v
@@ -2,6 +2,7 @@ Require Export Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterf
         Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties.
 
 Require Import
+        Coq.Arith.PeanoNat
         Coq.FSets.FMapInterface
         Coq.FSets.FMapFacts
         Coq.FSets.FMapAVL
@@ -434,13 +435,13 @@ Module RangeTreeBag (X : OrderedType).
         eapply binsert_RepInv; eapply containerCorrect; eauto.
         eapply binsert_RepInv; eapply bempty_RepInv.
       - rewrite <- is_eq.
-        rewrite binsert_enumerate_weak with (RepInv0 := RepInv) (ValidUpdate0 := ValidUpdate) in H;
+        rewrite binsert_enumerate_weak with (RepInv := RepInv) (ValidUpdate := ValidUpdate) in H;
           intuition; subst.
         destruct (FindWithDefault_dec (projection item') bempty container)
           as [ [bag' (mapsto & equality)] | (not_found & equality) ];
         rewrite equality in *; clear equality.
         eapply containerCorrect; eauto.
-        rewrite benumerate_empty_eq_nil with (RepInv0 := RepInv) (ValidUpdate0 := ValidUpdate) in H0;
+        rewrite benumerate_empty_eq_nil with (RepInv := RepInv) (ValidUpdate := ValidUpdate) in H0;
           simpl in H0; intuition.
         reflexivity.
         destruct (FindWithDefault_dec (projection item') bempty container)
@@ -565,7 +566,7 @@ Module RangeTreeBag (X : OrderedType).
       rewrite values_add_not_in by assumption.
       simpl.
       rewrite binsert_enumerate.
-      rewrite benumerate_empty_eq_nil with (RepInv0 := RepInv) (ValidUpdate0 := ValidUpdate); eauto.
+      rewrite benumerate_empty_eq_nil with (RepInv := RepInv) (ValidUpdate := ValidUpdate); eauto.
       apply bempty_RepInv.
     Qed.
 
@@ -578,7 +579,7 @@ Module RangeTreeBag (X : OrderedType).
       pose proof (RangeTreeBag_btraverse_closed container (minkey, maxkey)).
       rewrite <- Heqbs in H; clear Heqbs.
       rewrite length_flatten.
-      setoid_rewrite Plus.plus_comm at 1.
+      setoid_rewrite Nat.add_comm at 1.
       replace (fun (y : TKey * BagType) (x : nat) => bcount (snd y) searchterm + x)
       with (compose plus (fun (y : TKey * BagType) => bcount (snd y) searchterm)) by reflexivity.
       rewrite !foldright_compose.
diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/TreeBags.v b/src/QueryStructure/Implementation/DataStructures/Bags/TreeBags.v
index 3684daa8e..bdb8de851 100644
--- a/src/QueryStructure/Implementation/DataStructures/Bags/TreeBags.v
+++ b/src/QueryStructure/Implementation/DataStructures/Bags/TreeBags.v
@@ -4,6 +4,7 @@ Require Export Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterf
         Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties.
 Require Import
         Coq.FSets.FMapInterface Coq.FSets.FMapFacts
+        Coq.Arith.PeanoNat
         Fiat.Common
         Fiat.Common.List.ListFacts
         Fiat.Common.List.FlattenList
@@ -203,13 +204,13 @@ Module TreeBag (Import M: WS).
         eapply binsert_RepInv; eapply containerCorrect; eauto.
         eapply binsert_RepInv; eapply bempty_RepInv.
       - rewrite <- is_eq.
-        rewrite binsert_enumerate_weak with (RepInv0 := RepInv) (ValidUpdate0 := ValidUpdate) in H; intuition; subst.
+        rewrite binsert_enumerate_weak with (RepInv := RepInv) (ValidUpdate := ValidUpdate) in H; intuition; subst.
 
         destruct (FindWithDefault_dec (projection item') bempty container)
           as [ [bag' (mapsto & equality)] | (not_found & equality) ];
         rewrite equality in *; clear equality.
         eapply containerCorrect; eauto.
-        rewrite benumerate_empty_eq_nil with (RepInv0 := RepInv) (ValidUpdate0 := ValidUpdate) in H0;
+        rewrite benumerate_empty_eq_nil with (RepInv := RepInv) (ValidUpdate := ValidUpdate) in H0;
           simpl in H0; intuition.
         reflexivity.
         destruct (FindWithDefault_dec (projection item') bempty container)
@@ -368,7 +369,7 @@ Module TreeBag (Import M: WS).
       simpl.
 
       rewrite binsert_enumerate.
-      rewrite benumerate_empty_eq_nil with (RepInv0 := RepInv) (ValidUpdate0 := ValidUpdate); eauto.
+      rewrite benumerate_empty_eq_nil with (RepInv := RepInv) (ValidUpdate := ValidUpdate); eauto.
       apply bempty_RepInv.
     Qed.
 
@@ -396,7 +397,7 @@ Module TreeBag (Import M: WS).
       + rewrite length_flatten.
         rewrite (fold_over_Values _ _ (fun acc bag => acc + bcount bag search_term)) by eauto.
         rewrite <- fold_left_rev_right.
-        setoid_rewrite Plus.plus_comm at 1.
+        setoid_rewrite Nat.add_comm at 1.
         replace (fun (y : BagType) (x : nat) => bcount y search_term + x)
         with (compose plus (fun bag => bcount bag search_term)) by reflexivity.
         rewrite !foldright_compose.
diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/TrieBags.v b/src/QueryStructure/Implementation/DataStructures/Bags/TrieBags.v
index f36a69e4c..696f21eaf 100644
--- a/src/QueryStructure/Implementation/DataStructures/Bags/TrieBags.v
+++ b/src/QueryStructure/Implementation/DataStructures/Bags/TrieBags.v
@@ -1078,7 +1078,7 @@ Module TrieBag (X:OrderedType).
         replaceXMapfold.
         unfold XMap.fold at 2.
 
-        rewrite Permutation_KeyBasedPartition with (key0 := key0)
+        rewrite Permutation_KeyBasedPartition with (key := key0)
                                                      (bst_m := SubTrieMapBST H1).
 
         pose proof (@partition_after_KeyBasedPartition_and_add
@@ -1980,9 +1980,9 @@ Module TrieBag (X:OrderedType).
             rewrite filter_Prefix; eauto.
           + rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
             match goal with
-            | [ H0 : TrieOK _ _ |- _ ] =>
-                rewrite Permutation_KeyBasedPartition with (key0 := key0)
-                                                           (bst_m := SubTrieMapBST H0)
+            | [ H : TrieOK _ _ |- _ ] =>
+                rewrite Permutation_KeyBasedPartition with (key := key0)
+                                                           (bst_m := SubTrieMapBST H)
             end.
             simpl.
             apply find_2 in e0.
@@ -2012,9 +2012,9 @@ Module TrieBag (X:OrderedType).
           + rewrite filter_Prefix; eauto.
           + rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
             match goal with
-            | [ H : TrieOK _ _ |- _ ] =>
-                rewrite Permutation_KeyBasedPartition with (key0 := key0)
-                                                           (bst_m := SubTrieMapBST' H)
+            | [ H0 : TrieOK _ _ |- _ ] =>
+                rewrite Permutation_KeyBasedPartition with (key := key0)
+                                                           (bst_m := SubTrieMapBST' H0)
             end.
             simpl in *.
             match goal with
@@ -2209,7 +2209,7 @@ Module TrieBag (X:OrderedType).
               eapply filter_negb_Prefix; eauto; reflexivity.
             + simpl.
               rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
-              rewrite Permutation_KeyBasedPartition with (key0 := key0)
+              rewrite Permutation_KeyBasedPartition with (key := key0)
                                                            (bst_m := SubTrieMapBST containerCorrect).
               simpl in *.
               apply find_2 in e1.
@@ -2264,7 +2264,7 @@ Module TrieBag (X:OrderedType).
               eapply filter_negb_Prefix; eauto; reflexivity.
             + simpl.
               rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
-              rewrite Permutation_KeyBasedPartition with (key0 := key0)
+              rewrite Permutation_KeyBasedPartition with (key := key0)
                                                            (bst_m := SubTrieMapBST containerCorrect).
               simpl.
               rewrite <- (@not_find_in_iff _ (XMap.Bst (SubTrieMapBST' containerCorrect)) key0) in e1.
@@ -2338,7 +2338,7 @@ Module TrieBag (X:OrderedType).
             + rewrite (H (l ++ [key0])); simpl; eauto.
               rewrite partition_filter_eq.
               rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
-              rewrite Permutation_KeyBasedPartition with (key0 := key0)
+              rewrite Permutation_KeyBasedPartition with (key := key0)
                                                            (bst_m := SubTrieMapBST containerCorrect).
               simpl.
               apply find_2 in e1.
@@ -2373,7 +2373,7 @@ Module TrieBag (X:OrderedType).
               eapply filter_Prefix; eauto.
             + simpl.
               rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
-              rewrite Permutation_KeyBasedPartition with (key0 := key0)
+              rewrite Permutation_KeyBasedPartition with (key := key0)
                                                            (bst_m := SubTrieMapBST containerCorrect).
               rewrite <- (@not_find_in_iff _ (XMap.Bst (SubTrieMapBST' containerCorrect)) key0) in e1.
               pose proof (KeyBasedPartition_fst_singleton_None key0 (XMap.Bst (SubTrieMapBST containerCorrect)) e1) as singleton.
@@ -2559,7 +2559,7 @@ Module TrieBag (X:OrderedType).
               f_equiv.
               * symmetry; f_equiv; eapply filter_Prefix; eauto.
               * rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
-                rewrite Permutation_KeyBasedPartition with (key0 := key0)
+                rewrite Permutation_KeyBasedPartition with (key := key0)
                                                              (bst_m := SubTrieMapBST containerCorrect).
                 rewrite (Permutation_benumerate_add key0 bag'' (XMap.Bst (SubTrieMapBST containerCorrect))).
                 rewrite map_app, flatten_app.
@@ -2636,7 +2636,7 @@ Module TrieBag (X:OrderedType).
               * rewrite filter_Prefix; eauto; reflexivity.
               * simpl.
                 rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
-                rewrite Permutation_KeyBasedPartition with (key0 := key0)
+                rewrite Permutation_KeyBasedPartition with (key := key0)
                                                              (bst_m := SubTrieMapBST containerCorrect).
                 simpl.
                 rewrite <- (@not_find_in_iff _ (XMap.Bst (SubTrieMapBST' containerCorrect)) key0) in e1.
@@ -2700,7 +2700,7 @@ Module TrieBag (X:OrderedType).
             + rewrite (H (l ++ [key0])); simpl; eauto.
               rewrite partition_filter_eq.
               rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
-              rewrite Permutation_KeyBasedPartition with (key0 := key0)
+              rewrite Permutation_KeyBasedPartition with (key := key0)
                                                            (bst_m := SubTrieMapBST containerCorrect).
               simpl.
               apply find_2 in e1.
@@ -2735,7 +2735,7 @@ Module TrieBag (X:OrderedType).
             + rewrite filter_Prefix; eauto.
             + simpl.
               rewrite <- (fun H => @fold_1 _ m H (list BagType) [ ] (fun k trie a => Trie_enumerate trie ++ a)) by eauto.
-              rewrite Permutation_KeyBasedPartition with (key0 := key0)
+              rewrite Permutation_KeyBasedPartition with (key := key0)
                                                            (bst_m := SubTrieMapBST containerCorrect).
               rewrite <- (@not_find_in_iff _ (XMap.Bst (SubTrieMapBST' containerCorrect)) key0) in e1.
               pose proof (KeyBasedPartition_fst_singleton_None key0 (XMap.Bst (SubTrieMapBST containerCorrect)) e1) as singleton.
diff --git a/src/QueryStructure/Implementation/Operations/General/InsertRefinements.v b/src/QueryStructure/Implementation/Operations/General/InsertRefinements.v
index 8a5bcae96..eade4097e 100644
--- a/src/QueryStructure/Implementation/Operations/General/InsertRefinements.v
+++ b/src/QueryStructure/Implementation/Operations/General/InsertRefinements.v
@@ -660,7 +660,6 @@ Section InsertRefinements.
           as rewriteSat
             by (apply functional_extensionality; intros; rewrite GetRelDropConstraints;
                 reflexivity).
-      rewrite GetRelDropConstraints in H', H'',  H''''.
       setoid_rewrite rewriteSat in H''''; clear rewriteSat.
       (* Resume not-terribleness *)
       generalize (Iterate_Decide_Comp_BoundedIndex _ _ H''') as H3';
diff --git a/src/QueryStructure/Specification/Representation/QueryStructure.v b/src/QueryStructure/Specification/Representation/QueryStructure.v
index 9c5c5aad8..d40f88542 100644
--- a/src/QueryStructure/Specification/Representation/QueryStructure.v
+++ b/src/QueryStructure/Specification/Representation/QueryStructure.v
@@ -50,7 +50,7 @@ Section BuildQueryStructureConstraints.
     (* No need to check if the indices are in the list of Relations, because
      they are Bounded Strings. *)
     unfold crossRelationR, GetNRelSchemaHeading, GetNRelSchema; simpl.
-    rewrite H, H0;  exact (Some c).
+    rewrite e, e0;  exact (Some c).
   Defined.
 
   Fixpoint BuildQueryStructureConstraints'