proposition: Lemma zexp_mult : forall (x : R) m n x_ xm_, (x[//]x_) [^^] (m * n) [=] ((x[//]x_) [^^] (m) [//]xm_) [^^] (n).
proof: Proof. intros x m n Hx He. pattern n in |- *. apply pred_succ_Z_ind. rewrite <- Zmult_0_r_reverse. algebra. intros. rewrite Zmult_plus_distr_r. astepr (((x[//]Hx) [^^] (m) [//]He) [^^] (n0) [*] (x[//]Hx) [^^] (m)). rewrite Zmult_1_r. astepl ((x[//]Hx) [^^] (m * n0) [*] (x[//]Hx) [^^] (m)). algebra. intros. rewrite CornBasics.Zmult_minus_distr_r. astepr (((x[//]Hx) [^^] (m) [//]He) [^^] (n0) [/] (x[//]Hx) [^^] (m) [//]He). rewrite Zmult_1_r. astepl ((x[//]Hx) [^^] (m * n0) [/] (x[//]Hx) [^^] (m) [//]He). algebra. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)