proposition: Lemma Log_div : forall x y Hx Hy Hy' Hxy, Log (x[/] y[//]Hy') Hxy [=] Log x Hx[-]Log y Hy.
proof: Proof. intros x y Hx Hy Hy' Hxy. unfold cg_minus in |- *. apply eq_transitive_unfolded with (Log _ (mult_resp_pos _ _ _ Hx (recip_resp_pos _ _ Hy' Hy))). apply Log_wd; rational. Step_final (Log _ Hx[+]Log _ (recip_resp_pos _ _ Hy' Hy)). Qed.
imports: CoRN.transc.TaylorSeries