proposition: Lemma tech_pow_Rmult : forall (x:R) (n:nat), x * x ^ n = x ^ S n.
proof: Proof. simple induction n; simpl; trivial. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac