diff options
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. |