diff options
Diffstat (limited to 'theories/NArith/Ndec.v')
| -rw-r--r-- | theories/NArith/Ndec.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index f8db75484..6c9a03a65 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -119,11 +119,11 @@ Lemma Nneq_elim a a' : N.odd a = negb (N.odd a') \/ N.eqb (N.div2 a) (N.div2 a') = false. Proof. - intros. cut (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')). - intros. elim H0. intro. right. apply Ndiv2_bit_neq. assumption. - assumption. - intro. left. assumption. - case (N.odd a), (N.odd a'); auto. + intros. + enough (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')) as []. + - right. apply Ndiv2_bit_neq; assumption. + - left. assumption. + - case (N.odd a), (N.odd a'); auto. Qed. Lemma Ndouble_or_double_plus_un a : |