proposition: Lemma Zero_leEq_Log : forall (x : IR) Hx, [1] [<=] x -> [0] [<=] Log x Hx.
proof: Proof. intros x Hx H. astepl (Log (Exp [0]) (Exp_pos [0])). apply Log_resp_leEq. astepl OneR; auto. Qed.
imports: CoRN.transc.TaylorSeries