proposition: Lemma Log_cancel_less : forall x y Hx Hy, Log x Hx [<] Log y Hy -> x [<] y.
proof: Proof. intros x y Hx Hy H. astepl (Exp (Log x Hx)). astepr (Exp (Log y Hy)). apply Exp_resp_less; auto. Qed.
imports: CoRN.transc.TaylorSeries