proposition: Lemma RInt_val_swap : forall (f : R -> V) (a b : R) (n : nat), RInt_val f a b n = opp (RInt_val f b a n).
proof: Proof. intros f a b n. rewrite /RInt_val. rewrite -Riemann_sum_opp. rewrite unif_part_bound. elim: (unif_part b a n) => [ | x1 s IH] /=. by []. clear -IH. rewrite rev_cons. destruct s as [ | x2 s]. by []. rewrite SF_cons_f2. 2: by apply Nat.lt_0_succ. rewrite Riemann_sum_cons /= -IH => {IH}. rewrite scal_opp_r -scal_opp_l /=. rewrite rev_cons. elim: (rev s) => {s} /= [ | x3 s IH]. rewrite /Riemann_sum /=. apply (f_equal2 (fun x y => plus (scal x (f y)) _)) ; rewrite /Rdiv /opp /= ; ring. rewrite !SF_cons_f2 ; try (by rewrite size_rcons ; apply Nat.lt_0_succ). rewrite !Riemann_sum_cons /= IH !plus_assoc => {IH}. apply (f_equal (fun x => plus x _)). rewrite plus_comm. apply f_equal. apply (f_equal2 (fun x y => scal (x - x3) (f ((x3 + y) / 2)))) ; clear ; by elim: s. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy