diff options
| author | Jasper Hugunin | 2020-10-08 17:16:38 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-08 17:16:38 -0700 |
| commit | 4ffac2e8788dfc29b03a9eb19e427d8e4bb0961d (patch) | |
| tree | 7a012c7de5f367ec43d2270a5a40d07557be41ba | |
| parent | c5f76701ba9c42f8c4ce9881f05904dff677050c (diff) | |
Modify Numbers/Integer/Abstract/ZPow.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPow.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index bec77fd136..9557212a86 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -73,7 +73,7 @@ Qed. Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b. Proof. - intros. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ. + intros a b ?. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ. reflexivity. symmetry. now apply pow_opp_even. Qed. @@ -119,7 +119,7 @@ Qed. Lemma abs_pow : forall a b, abs (a^b) == (abs a)^b. Proof. intros a b. - destruct (Even_or_Odd b). + destruct (Even_or_Odd b) as [H|H]. rewrite pow_even_abs by trivial. apply abs_eq, pow_nonneg, abs_nonneg. rewrite pow_odd_abs_sgn by trivial. |