diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/QArith/Qpower.v | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/QArith/Qpower.v')
| -rw-r--r-- | theories/QArith/Qpower.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index efaefbb7..fa341dd9 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -59,7 +59,7 @@ Qed. Lemma Qmult_power : forall a b n, (a*b)^n == a^n*b^n. Proof. - intros a b [|n|n]; simpl; + intros a b [|n|n]; simpl; try rewrite Qmult_power_positive; try rewrite Qinv_mult_distr; reflexivity. @@ -73,7 +73,7 @@ Qed. Lemma Qinv_power : forall a n, (/a)^n == /a^n. Proof. - intros a [|n|n]; simpl; + intros a [|n|n]; simpl; try rewrite Qinv_power_positive; reflexivity. Qed. @@ -173,8 +173,8 @@ Qed. Lemma Qpower_mult : forall a n m, a^(n*m) == (a^n)^m. Proof. -intros a [|n|n] [|m|m]; simpl; - try rewrite Qpower_positive_1; +intros a [|n|n] [|m|m]; simpl; + try rewrite Qpower_positive_1; try rewrite Qpower_mult_positive; try rewrite Qinv_power_positive; try rewrite Qinv_involutive; |