diff options
| author |  emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-20 18:24:50 +0000 |
|---|---|---|
| committer | emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-20 18:24:50 +0000 |
| commit | d8a2c246510af26104fb16fb8ac7c266341c2f8b (patch) | |
| tree | 09cfed2be0d53047820e8f0a32eab5478229464e /theories/NArith/Nnat.v | |
| parent | b42da20a5b89a266b1a3964819d03b5ef7214688 (diff) | |
Changed the definition of Nminus in BinNat.v by removing comparison.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10130 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith/Nnat.v')
| -rw-r--r-- | theories/NArith/Nnat.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 76a3d616c..55c3a3b78 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -120,8 +120,11 @@ Proof. destruct a; destruct a'; simpl; auto with arith. case_eq (Pcompare p p0 Eq); simpl; intros. rewrite (Pcompare_Eq_eq _ _ H); auto with arith. - symmetry; apply not_le_minus_0. - generalize (nat_of_P_lt_Lt_compare_morphism _ _ H); auto with arith. + rewrite Pminus_mask_diag. simpl. apply minus_n_n. + rewrite Pminus_mask_Lt. pose proof (nat_of_P_lt_Lt_compare_morphism _ _ H). simpl. + symmetry; apply not_le_minus_0. auto with arith. assumption. + pose proof (Pminus_mask_Gt p p0 H) as H1. destruct H1 as [q [H1 _]]. rewrite H1; simpl. + replace q with (Pminus p p0) by (unfold Pminus; now rewrite H1). apply nat_of_P_minus_morphism; auto. Qed. |