proposition: Lemma RInt_val_comp_opp (f : R -> V) (a b : R) (n : nat) : RInt_val (fun x => f (- x)) a b n = opp (RInt_val f (- a) (- b) n).
proof: Proof. rewrite /RInt_val. replace (unif_part (- a) (- b) n) with (map Ropp (unif_part a b n)). elim: (unif_part a b n) {1}0 {2}0 => /= [ | x1 s IH] x0 x0'. rewrite /Riemann_sum /=. rewrite opp_zero //. destruct s as [ | x2 s]. rewrite /Riemann_sum /=. rewrite opp_zero //. rewrite (SF_cons_f2 _ x1) ; try by apply Nat.lt_0_succ. rewrite (SF_cons_f2 _ (- x1)) ; try by apply Nat.lt_0_succ. rewrite !Riemann_sum_cons /=. rewrite opp_plus. apply f_equal2. rewrite -scal_opp_l. apply (f_equal2 (fun x y => scal x (f y))) ; rewrite /Rdiv /opp /= ; field. by apply IH. apply eq_from_nth with 0. by rewrite size_map !size_mkseq. rewrite size_map => i Hi. rewrite (nth_map 0 0) => //. rewrite size_mkseq in Hi. rewrite !nth_mkseq => //. field. now rewrite -S_INR ; apply not_0_INR, sym_not_eq, O_S. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy