diff --git a/coq-menhirlib/src/Alphabet.v b/coq-menhirlib/src/Alphabet.v
index 8cc4ef3a..beaa3268 100644
--- a/coq-menhirlib/src/Alphabet.v
+++ b/coq-menhirlib/src/Alphabet.v
@@ -73,7 +73,7 @@ rewrite Nat.compare_eq_iff in *; destruct H; assumption.
 rewrite <- nat_compare_lt in *.
 apply (Nat.lt_trans _ _ _ H H0).
 rewrite <- nat_compare_gt in *.
-apply (gt_trans _ _ _ H H0).
+apply (Nat.lt_trans _ _ _ H0 H).
 Qed.
 
 (** A pair of comparable is comparable. **)
diff --git a/coq-menhirlib/src/Interpreter_complete.v b/coq-menhirlib/src/Interpreter_complete.v
index f79e09aa..10d5cb79 100644
--- a/coq-menhirlib/src/Interpreter_complete.v
+++ b/coq-menhirlib/src/Interpreter_complete.v
@@ -786,9 +786,9 @@ Proof.
   - assert (Hptd := next_ptd_cost ptd). destruct next_ptd=>//. by rewrite Hptd.
   - rewrite Nat.add_0_r. assert (IH1 := IH ptd). destruct next_ptd_iter as [ptd'|].
     + specialize (IH ptd'). destruct next_ptd_iter as [ptd''|].
-      * by rewrite IH1 IH -!plus_assoc.
-      * rewrite IH1. by apply plus_lt_compat_l.
-    + by apply lt_plus_trans.
+      * by rewrite IH1 IH -!Nat.add_assoc.
+      * rewrite IH1. by apply Nat.add_lt_mono_l.
+    + by apply Nat.lt_le_trans with (1 := IH1), Nat.le_add_r.
 Qed.
 
 (** We now prove the top-level parsing function. The only thing that
@@ -814,8 +814,8 @@ Proof.
   destruct next_ptd_iter.
   - destruct Hparse as (? & -> & ?). apply (f_equal S) in Hcost.
     rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost. rewrite Hcost.
-    apply le_lt_n_Sm, le_plus_l.
-  - rewrite Hparse. split; [|split]=>//. apply lt_le_S in Hcost.
+    apply Nat.lt_succ_r, Nat.le_add_r.
+  - rewrite Hparse. split; [|split]=>//. apply Nat.le_succ_l in Hcost.
     by rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost.
 Qed.