From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- theories/QArith/Qpower.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theories/QArith/Qpower.v') 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; -- cgit v1.2.3