proposition: Lemma ex_RInt_ext : forall (f g : R -> V) (a b : R), (forall x, Rmin a b < x < Rmax a b -> f x = g x) -> ex_RInt f a b -> ex_RInt g a b.
proof: Proof. intros f g a b Heq [If Hex]. exists If. revert Hex. now apply is_RInt_ext. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy