proposition: Lemma is_RInt_swap : forall (f : R -> V) (a b : R) (If : V), is_RInt f b a If -> is_RInt f a b (opp If).
proof: Proof. unfold is_RInt. intros f a b If HIf. rewrite -scal_opp_one /=. apply filterlim_ext with (fun ptd => scal (opp (one : R)) (scal (sign (a - b)) (Riemann_sum f ptd))). intros x. rewrite scal_assoc. apply (f_equal (fun s => scal s _)). rewrite /mult /opp /one /=. by rewrite -(Ropp_minus_distr' b a) sign_opp /= Ropp_mult_distr_l_reverse Rmult_1_l. unfold Riemann_fine. rewrite Rmin_comm Rmax_comm. apply filterlim_comp with (1 := HIf). 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