proposition: Lemma RInt_ext (f g : R -> V) (a b : R) : (forall x, Rmin a b < x < Rmax a b -> f x = g x) -> RInt f a b = RInt g a b.
proof: Proof. intros Hfg. apply eq_close. apply: close_iota ; split ; apply is_RInt_ext. exact Hfg. intros t Ht. now apply sym_eq, Hfg. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy