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