proposition: Lemma is_RInt_scal : forall (f : R -> V) (a b : R) (k : R) (If : V), is_RInt f a b If -> is_RInt (fun y => scal k (f y)) a b (scal k If).
proof: Proof. intros f a b k If Hf. apply filterlim_ext with (fun ptd => scal k (scal (sign (b - a)) (Riemann_sum f ptd))). intros ptd. rewrite Riemann_sum_scal. rewrite 2!scal_assoc. apply (f_equal (fun x => scal x _)). apply Rmult_comm. apply filterlim_comp with (1 := Hf). apply: filterlim_scal_r. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy