proposition: Lemma RInt_val_ext (f g : R -> V) (a b : R) (n : nat) : (forall x, Rmin a b <= x <= Rmax a b -> f x = g x) -> RInt_val g a b n = RInt_val f a b n.
proof: Proof. wlog: a b / (a <= b) => [Hw | Hab]. case: (Rle_lt_dec a b) => Hab. by apply Hw. rewrite Rmin_comm Rmax_comm => Heq. apply Rlt_le in Hab. rewrite RInt_val_swap Hw => //=. apply sym_eq ; by apply RInt_val_swap. rewrite /Rmin /Rmax ; case: Rle_dec => //= _ Heq. unfold RInt_val. set l := (SF_seq_f2 (fun x y : R => (x + y) / 2) (unif_part a b n)). assert (forall i, (i < size (SF_ly l))%nat -> f (nth 0 (SF_ly l) i) = g (nth 0 (SF_ly l) i)). move => i Hi. apply Heq. destruct (fun H0 => Riemann_fine_unif_part (fun x y : R => (x + y) / 2) a b n H0 Hab) as [H [H0 [H1 H2]]]. clear. intros a b Hab. lra. fold l in H, H0, H1, H2. rewrite -H1 -H2 ; split. apply Rle_trans with (head 0 (SF_ly l)). apply (H0 O). by apply Nat.lt_0_succ. apply sorted_head. by apply ptd_sort'. by []. apply Rle_trans with (last 0 (SF_ly l)). apply sorted_last. by apply ptd_sort'. by []. rewrite -!nth_last SF_size_ly SF_size_lx SF_size_f2 size_mkseq. simpl Peano.pred. replace (nth (SF_h l) (SF_lx l) (S n)) with (nth 0 (SF_lx l) (S n)). apply (H0 n). rewrite SF_size_f2 size_mkseq /=. by apply Nat.lt_succ_diag_r. rewrite SF_lx_f2. assert (size (unif_part a b n) = S (S n)). by apply size_mkseq. elim: (S n) (unif_part a b n) H3 ; simpl ; clear ; intros. destruct unif_part0 ; simpl => //. replace unif_part0 with (head 0 unif_part0 :: behead unif_part0). apply H. destruct unif_part0 ; by intuition. destruct unif_part0 ; by intuition. by apply Nat.lt_0_succ. move: H => {Heq}. apply SF_cons_ind with (s := l) => {l} [x0 | h0 s IH] /= Heq. by []. rewrite !Riemann_sum_cons. apply (f_equal2 (fun x y => plus (scal (SF_h s - fst h0) x) y)). by apply sym_eq, (Heq O), Nat.lt_0_succ. apply IH => i Hi. now apply (Heq (S i)); apply ->Nat.succ_lt_mono. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy