proposition: Lemma ex_RInt_const : forall (a b : R) (v : V), ex_RInt (fun _ => v) a b.
proof: Proof. intros a b v. exists (scal (b - a) v). apply is_RInt_const. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy