proposition: Lemma One_leEq_Exp : forall x : IR, [0] [<=] x -> [1] [<=] Exp x.
proof: Proof. intros x H. astepl (Exp [0]). apply resp_leEq_char; auto. algebra. intro H0; astepl OneR. apply One_less_Exp; auto. Qed.
imports: CoRN.transc.TaylorSeries