proposition: Lemma is_RInt_minus : forall (f g : R -> V) (a b : R) (If Ig : V), is_RInt f a b If -> is_RInt g a b Ig -> is_RInt (fun y => minus (f y) (g y)) a b (minus If Ig).
proof: Proof. intros f g a b If Ig Hf Hg. apply filterlim_ext with (fun ptd => (plus (scal (sign (b - a)) (Riemann_sum f ptd)) (scal (opp 1) (scal (sign (b - a)) (Riemann_sum g ptd))))). intros ptd. rewrite Riemann_sum_minus. unfold minus. rewrite scal_opp_one. rewrite -scal_opp_r. apply sym_eq, @scal_distr_l. eapply filterlim_comp_2 with (1 := Hf). apply filterlim_comp with (1 := Hg). eapply @filterlim_scal_r. rewrite scal_opp_one. apply: filterlim_plus. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy