Add leb_not_le: (n <=? m) = false -> n > m.

1 files changed, 11 insertions, 0 deletions

diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index bde6f1bb4..ffa56a6c3 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -172,6 +172,17 @@ Proof.
  apply leb_le.
 Qed.
 
+
+Lemma leb_not_le n m : (n <=? m) = false -> n > m.
+Proof.
+  revert m; induction n; destruct m; simpl; intros H_nm.
+  - congruence.
+  - congruence.
+  - apply lt_succ_r, le_0_n.
+  - specialize (IHn _ H_nm).
+    now apply lt_succ_r in IHn.
+Qed.
+
 (** ** Decidability of equality over [nat]. *)
 
 Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}.