proposition: Lemma Log_less_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_less. astepr OneR; auto. Qed.
imports: CoRN.transc.TaylorSeries