diff options
| author | Jasper Hugunin | 2020-10-08 17:15:09 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-08 17:15:09 -0700 |
| commit | c5f76701ba9c42f8c4ce9881f05904dff677050c (patch) | |
| tree | 9998e4b1d5632f8fb96c96faf49ddb41489e8049 | |
| parent | d2e0606e3af5cfb6a059666641c9d57eb8464235 (diff) | |
Modify Numbers/Integer/Abstract/ZParity.v to compile with -mangle-names
| -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. |