proposition: Lemma is_RInt_const : forall (a b : R) (v : V), is_RInt (fun _ => v) a b (scal (b - a) v).
proof: Proof. intros a b v. apply filterlim_within_ext with (fun _ => scal (b - a) v). 2: apply filterlim_const. intros ptd [_ [Hhead Hlast]]. rewrite Riemann_sum_const. rewrite Hlast Hhead. rewrite scal_assoc. apply (f_equal (fun x => scal x v)). apply sym_eq, sign_min_max. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy