proposition: Lemma zexp_plus : forall (x : R) x_ m n, (x[//]x_) [^^] (m + n) [=] (x[//]x_) [^^] (m) [*] (x[//]x_) [^^] (n).
proof: Proof. intros x Hx; intros. pattern n in |- *. apply pred_succ_Z_ind. simpl in |- *. replace (m + 0)%Z with m. algebra. auto with zarith. intros. replace (m + (n0 + 1))%Z with (m + n0 + 1)%Z. astepl ((x[//]Hx) [^^] (m + n0) [*]x). astepr ((x[//]Hx) [^^] (m) [*] ((x[//]Hx) [^^] (n0) [*]x)). astepr ((x[//]Hx) [^^] (m) [*] (x[//]Hx) [^^] (n0) [*]x). algebra. auto with zarith. intros. replace (m + (n0 - 1))%Z with (m + n0 - 1)%Z. astepl ((x[//]Hx) [^^] (m + n0) [/] x[//]Hx). astepr ((x[//]Hx) [^^] (m) [*] ((x[//]Hx) [^^] (n0) [/] x[//]Hx)). astepr ((x[//]Hx) [^^] (m) [*] (x[//]Hx) [^^] (n0) [/] x[//]Hx). algebra. unfold Zminus in |- *. auto with zarith. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)