proposition: Lemma Log_recip_char : forall x Hx Hx' Hx'', Log ([1][/] x[//]Hx) Hx'[+]Log x Hx'' [=] [0].
proof: Proof. intros x Hx Hx' Hx''. astepl (Log _ (mult_resp_pos _ _ _ Hx' Hx'')). astepr (Log _ (pos_one IR)). apply Log_wd; rational. Qed.
imports: CoRN.transc.TaylorSeries