proposition: Lemma pow_RN_plus : forall (x:R) (n m:nat), x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m.
proof: Proof. intros x n m H. apply (Rmult_eq_reg_r (x ^ m)); cycle 1. { now apply pow_nonzero. } rewrite Rmult_assoc, Rmult_inv_l, Rmult_1_r by (now apply pow_nonzero). now rewrite pow_add. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac