proposition: Lemma is_RInt_opp : forall (f : R -> V) (a b : R) (If : V), is_RInt f a b If -> is_RInt (fun y => opp (f y)) a b (opp If).
proof: Proof. intros f a b If Hf. apply filterlim_ext with (fun ptd => (scal (opp 1) (scal (sign (b - a)) (Riemann_sum f ptd)))). intros ptd. rewrite Riemann_sum_opp. rewrite scal_opp_one. apply sym_eq, scal_opp_r. apply filterlim_comp with (1 := Hf). rewrite -(scal_opp_one If). 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