proposition: Lemma Log_div' : forall x y z Hx Hy Hy' Hz, z [=] (x[/] y[//]Hy') -> Log z Hz [=] Log x Hx[-]Log y Hy.
proof: Proof. intros x y z Hx Hy Hy' Hz H. Step_final (Log _ (div_resp_pos _ _ _ Hy' Hy Hx)). Qed.
imports: CoRN.transc.TaylorSeries