diff options
| author |  roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-05 16:27:30 +0000 |
|---|---|---|
| committer | roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-05 16:27:30 +0000 |
| commit | 272c6e29d97367ffccf973c59ed59ac064a9be0a (patch) | |
| tree | 2d025baa8e967f926433b046ba29511d3f051f72 /theories/QArith/Qpower.v | |
| parent | 16d82fecd6b070de30f0047b0ff9930ee8d67f02 (diff) | |
Added Qpower_mult theorem.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9946 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/QArith/Qpower.v')
| -rw-r--r-- | theories/QArith/Qpower.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index d50443498..7db520b95 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -137,3 +137,25 @@ case_eq ((n ?= m)%positive Eq); intros H0; simpl; assumption. Qed. +Lemma Qpower_mult_positive : forall a n m, Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m. +Proof. +intros a n m. +induction n using Pind. + reflexivity. +rewrite Pmult_Sn_m. +rewrite Pplus_one_succ_l. +do 2 rewrite Qpower_plus_positive. +rewrite IHn. +rewrite Qmult_power_positive. +reflexivity. +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; + try rewrite Qpower_mult_positive; + try rewrite Qinv_power_positive; + try rewrite Qinv_involutive; + try reflexivity. +Qed.
\ No newline at end of file |