proposition: Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2.
proof: Proof. intros; induction n2 as [| n2 Hrecn2]. - simpl; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ]. - replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat. + replace (S n2) with (n2 + 1)%nat by ring. do 2 rewrite pow_add. rewrite Hrecn2. simpl. ring. + ring. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac