diff options
| author |  Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-03 20:45:13 +0200 |
|---|---|---|
| committer | Raphaël Monat <raphael.monat@ens-lyon.org> | 2017-10-03 20:45:13 +0200 |
| commit | b4b778f1a1657e0b65f5ac3fe466ca9a1e8d55d3 (patch) | |
| tree | 7949298d0ea43c7d53116b3d2ca75f708ef15d88 /theories | |
| parent | e664022ba1314d866e4e148d5f5f925654db0487 (diff) | |
Changed the statement of leb_not_le; shortened the proof
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Arith/PeanoNat.v | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index ffa56a6c3..95fd4cf86 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -172,15 +172,9 @@ Proof. apply leb_le. Qed. - -Lemma leb_not_le n m : (n <=? m) = false -> n > m. +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. + now rewrite <- leb_le, <- not_true_iff_false. Qed. (** ** Decidability of equality over [nat]. *) |