proposition: Lemma is_RInt_exp : forall a b, is_RInt exp a b (exp b - exp a).
proof: Proof. intros a b. apply: is_RInt_derive. intros x _. apply is_derive_Reals, derivable_pt_lim_exp. intros x _. apply continuity_pt_filterlim. apply derivable_continuous_pt. apply derivable_pt_exp. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis