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 /contrib/setoid_ring | |
| 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 'contrib/setoid_ring')
| -rw-r--r-- | contrib/setoid_ring/Ring_zdiv.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/contrib/setoid_ring/Ring_zdiv.v b/contrib/setoid_ring/Ring_zdiv.v index 9b102c28c..44874e547 100644 --- a/contrib/setoid_ring/Ring_zdiv.v +++ b/contrib/setoid_ring/Ring_zdiv.v @@ -40,10 +40,9 @@ destruct a; intros; simpl; auto. rewrite (Pcompare_Eq_eq _ _ H). assert (HH: forall p, Pminus p p = xH). intro p0; unfold Pminus; rewrite Pminus_mask_diag; auto. - simpl; auto. - generalize (Pplus_minus _ _ H). - case (p - b)%positive; intros; subst; - unfold Nplus; rewrite Pplus_comm; trivial. + apply Pcompare_Eq_eq in H. now rewrite Pminus_mask_diag. + pose proof (Pminus_mask_Gt p b H) as H1. destruct H1 as [d [H2 [H3 _]]]. + rewrite H2. rewrite <- H3. unfold Nplus. now rewrite Pplus_comm. Qed. Theorem Z_of_N_plus: |