proposition: Lemma Log_cancel_leEq : 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_leEq; auto. Qed.
imports: CoRN.transc.TaylorSeries