diff options
Diffstat (limited to 'theories/Arith/Even.v')
| -rw-r--r-- | theories/Arith/Even.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index baf119732..a1d0e9fcc 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -38,7 +38,7 @@ Hint Constructors odd: arith. Lemma even_equiv : forall n, even n <-> Nat.Even n. Proof. - fix 1. + fix even_equiv 1. destruct n as [|[|n]]; simpl. - split; [now exists 0 | constructor]. - split. @@ -52,7 +52,7 @@ Qed. Lemma odd_equiv : forall n, odd n <-> Nat.Odd n. Proof. - fix 1. + fix odd_equiv 1. destruct n as [|[|n]]; simpl. - split. + inversion_clear 1. |