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