proposition: Lemma Rpow_mult_distr : forall (x y:R) (n:nat), (x * y) ^ n = x^n * y^n.
proof: Proof. intros x y n ; induction n. - field. - simpl. repeat (rewrite Rmult_assoc) ; apply Rmult_eq_compat_l. rewrite IHn ; field. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac