proposition: Lemma powerRZ_add : forall (x:R) (n m:Z), x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m.
proof: Proof. intros x [|n|n] [|m|m]; simpl; intros; auto with real. - rewrite Pos2Nat.inj_add; auto with real. - now apply powerRZ_pos_sub. - rewrite Rmult_comm. now apply powerRZ_pos_sub. - rewrite Pos2Nat.inj_add; auto with real. rewrite pow_add; auto with real. apply Rinv_mult. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac