proposition: Lemma opp_RInt_swap : forall f a b, ex_RInt f a b -> opp (RInt f a b) = RInt f b a.
proof: Proof. intros f a b [If HIf]. apply sym_eq, is_RInt_unique. apply: is_RInt_swap. apply RInt_correct. now exists If. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy