proposition: Lemma Rint_exp : forall a b, Rint exp a b (exp b - exp a).
proof: Proof. intros a b. apply Rint_derive2. intros; apply derivable_pt_lim_exp. intros; apply derivable_continuous_pt, derivable_pt_exp. Qed.
imports: Reals MyRfunctions Rintegral Lia