proposition: Lemma mult_zexp : forall (x y : R) z x_ y_ xy_, (x[*]y[//]xy_) [^^] (z) [=] (x[//]x_) [^^] (z) [*] (y[//]y_) [^^] (z).
proof: Proof. intros x y z Hx Hy Hp. pattern z in |- *. apply nats_Z_ind. intros. astepl ((x[*]y) [^]n). astepr (x[^]n[*]y[^]n). apply mult_nexp. intros. astepl ([1][/] (x[*]y[//]Hp) [^^] (n) [//]zexp_resp_ap_zero (x[*]y) n Hp). astepr (([1][/] (x[//]Hx) [^^] (n) [//]zexp_resp_ap_zero x n Hx) [*] ([1][/] (y[//]Hy) [^^] (n) [//]zexp_resp_ap_zero y n Hy)). astepl ([1][/] (x[*]y) [^]n[//]nexp_resp_ap_zero n Hp). astepr (([1][/] x[^]n[//]nexp_resp_ap_zero n Hx) [*] ([1][/] y[^]n[//]nexp_resp_ap_zero n Hy)). rstepr ([1][/] x[^]n[*]y[^]n[//] mult_resp_ap_zero _ _ _ (nexp_resp_ap_zero n Hx) (nexp_resp_ap_zero n Hy)). apply eq_div. algebra. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)