proposition: Lemma ex_RInt_scal : forall (f : R -> V) (a b : R) (k : R), ex_RInt f a b -> ex_RInt (fun y => scal k (f y)) a b.
proof: Proof. intros f a b k [If Hf]. exists (scal k If). now apply is_RInt_scal. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy