diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZParity.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZParity.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index 4b61b18479..0f68278cf0 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -19,19 +19,19 @@ Include NZParityProp Z Z ZP. Lemma odd_pred : forall n, odd (P n) = even n. Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. + intros n. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. Qed. Lemma even_pred : forall n, even (P n) = odd n. Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. + intros n. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. Qed. Lemma even_opp : forall n, even (-n) = even n. Proof. assert (H : forall n, Even n -> Even (-n)). intros n (m,H). exists (-m). rewrite mul_opp_r. now f_equiv. - intros. rewrite eq_iff_eq_true, !even_spec. + intros n. rewrite eq_iff_eq_true, !even_spec. split. rewrite <- (opp_involutive n) at 2. apply H. apply H. Qed. |