diff options
Diffstat (limited to 'theories/Arith/Even.v')
| -rw-r--r-- | theories/Arith/Even.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 9a84a7f2e..23dc1d259 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -145,7 +145,7 @@ Lemma even_mult_aux : forall n m, (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). Proof. - intros n; elim n; simpl in |- *; auto with arith. + intros n; elim n; simpl; auto with arith. intros m; split; split; auto with arith. intros H'; inversion H'. intros H'; elim H'; auto. |