proposition: Lemma Log_nexp : forall x n Hx Hxn, Log (x[^]n) Hxn [=] (nring n)[*]Log x Hx.
proof: Proof. induction n. intros Hx Hn. simpl. rstepr ([0]:IR). apply Log_one. intros Hx Hn. assert (X:[0][<]x[^]n). apply nexp_resp_pos. assumption. stepl (Log _ X[+]Log x Hx); [| apply eq_symmetric; apply (Log_mult _ _ X Hx)]. astepr ((nring n [+] [1])[*]Log x Hx). rstepr (nring n[*]Log x Hx[+]Log x Hx). apply bin_op_wd_unfolded; try apply eq_reflexive. apply IHn. Qed.
imports: CoRN.transc.TaylorSeries