diff options
Diffstat (limited to 'theories/Arith/Compare.v')
| -rw-r--r-- | theories/Arith/Compare.v | 30 |
1 files changed, 13 insertions, 17 deletions
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index b11f0517..06898658 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -6,21 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Compare.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Compare.v 9302 2006-10-27 21:21:17Z barras $ i*) (** Equality is decidable on [nat] *) + Open Local Scope nat_scope. -(* -Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p). -Proof sym_not_eq. -Hints Immediate not_eq_sym : arith. -*) Notation not_eq_sym := sym_not_eq. Implicit Types m n p q : nat. -Require Import Arith. +Require Import Arith_base. Require Import Peano_dec. Require Import Compare_dec. @@ -41,17 +37,17 @@ Proof le_lt_or_eq. (* By special request of G. Kahn - Used in Group Theory *) Lemma discrete_nat : - forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))). + forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))). Proof. -intros m n H. -lapply (lt_le_S m n); auto with arith. -intro H'; lapply (le_lt_or_eq (S m) n); auto with arith. -induction 1; auto with arith. -right; exists (n - S (S m)); simpl in |- *. -rewrite (plus_comm m (n - S (S m))). -rewrite (plus_n_Sm (n - S (S m)) m). -rewrite (plus_n_Sm (n - S (S m)) (S m)). -rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith. + intros m n H. + lapply (lt_le_S m n); auto with arith. + intro H'; lapply (le_lt_or_eq (S m) n); auto with arith. + induction 1; auto with arith. + right; exists (n - S (S m)); simpl in |- *. + rewrite (plus_comm m (n - S (S m))). + rewrite (plus_n_Sm (n - S (S m)) m). + rewrite (plus_n_Sm (n - S (S m)) (S m)). + rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith. Qed. Require Export Wf_nat. |