proposition: Lemma Log_zexp : forall x n Hx Hx0 Hxn, Log ((x[//]Hx0)[^^]n) Hxn [=] (zring n)[*]Log x Hx.
proof: Proof. intros x [|n|n] Hx Hx0 Hxn. simpl. rstepr ([0]:IR). algebra. assert (X:[0][<]x[^](nat_of_P n)). astepr ((x[//]Hx0)[^^]n). assumption. change (Log (x[^](nat_of_P n)) Hxn[=]zring (R:=IR) n[*]Log x Hx). astepl (nring (nat_of_P n)[*]Log x Hx). apply mult_wdl. apply eq_symmetric. rewrite <- inject_nat_convert. refine (zring_plus_nat IR (nat_of_P n)). simpl. change (Log (([1][/]x[//]Hx0)[^](nat_of_P n)) Hxn[=][--](zring n)[*]Log x Hx). assert (X:[0][<]([1][/]x[//]Hx0)). apply recip_resp_pos. assumption. astepl ((nring (nat_of_P n))[*](Log _ X)). astepl ((nring (nat_of_P n))[*]([--](Log _ Hx))). rstepl ([--](nring (nat_of_P n))[*](Log x Hx)). apply mult_wdl. apply un_op_wd_unfolded. rewrite <- inject_nat_convert. apply eq_symmetric. refine (zring_plus_nat IR (nat_of_P n)). Qed.
imports: CoRN.transc.TaylorSeries