proposition: Lemma tech_pow_Rplus : forall (x:R) (a n:nat), x ^ a + INR n * x ^ a = INR (S n) * x ^ a.
proof: Proof. intros; pattern (x ^ a) at 1; rewrite <- (let (H1, H2) := Rmult_ne (x ^ a) in H1); rewrite (Rmult_comm (INR n) (x ^ a)); rewrite <- (Rmult_plus_distr_l (x ^ a) 1 (INR n)); rewrite (Rplus_comm 1 (INR n)); rewrite <- (S_INR n); apply Rmult_comm. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac