proposition: Lemma RInt_val_comp_lin (f : R -> V) (u v : R) (a b : R) (n : nat) : scal u (RInt_val (fun x => f (u * x + v)) a b n) = RInt_val f (u * a + v) (u * b + v) n.
proof: Proof. rewrite /RInt_val. replace (unif_part (u * a + v) (u * b + v) n) with (map (fun x => u * x + v) (unif_part a b n)). elim: (unif_part a b n) {1}0 {2}0 => /= [ | x1 s IH] x0 x0'. by apply @scal_zero_r. destruct s as [ | x2 s]. by apply @scal_zero_r. rewrite (SF_cons_f2 _ x1) ; try by apply Nat.lt_0_succ. rewrite (SF_cons_f2 _ (u * x1 + v)) ; try by apply Nat.lt_0_succ. rewrite !Riemann_sum_cons /=. rewrite scal_distr_l. apply f_equal2. rewrite scal_assoc. apply (f_equal2 (fun x y => scal x (f y))) ; rewrite /mult /= ; 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