proposition: Lemma Log_resp_leEq : forall (x y : IR) Hx Hy, x [<=] y -> Log x Hx [<=] Log y Hy.
proof: Proof. intros x y Hx Hy; apply resp_leEq_char' with (P := fun x : IR => [0] [<] x). algebra. apply Log_resp_less. Qed.
imports: CoRN.transc.TaylorSeries