proposition: Lemma ad_SF_val_fun (f : R -> R) (a b : R) (n : nat) : ((a <= b) -> adapted_couple (SF_val_fun f a b n) a b (unif_part a b n) (SF_val_ly f a b n)) /\ (~(a <= b) -> adapted_couple (SF_val_fun f b a n) a b (unif_part b a n) (SF_val_ly f b a n)).
proof: Proof. wlog : a b / (a <= b) => Hw. split ; case: (Rle_dec a b) => // Hab _. by apply Hw. apply StepFun_P2 ; apply Hw ; by apply Rlt_le, Rnot_le_lt. split ; case: (Rle_dec a b) => // {Hw} Hab _. have : (a = head 0 (SF_lx (SF_val_seq f a b n))) ; [rewrite SF_lx_f2 /= ; (try by apply Nat.lt_0_succ) ; field ; apply Rgt_not_eq ; intuition | move => {2}->]. pattern b at 3 ; replace b with (last 0 (SF_lx (SF_val_seq f a b n))). rewrite -(SF_lx_f2 (fun x y => f ((x+y)/2)) (unif_part a b n)) ; try by apply Nat.lt_0_succ. rewrite /SF_val_ly -SF_ly_f2. unfold SF_val_fun, SF_fun_f2. replace (SF_seq_f2 (fun x y : R => f ((x + y) / 2)) (unif_part a b n)) with (SF_val_seq f a b n) by auto. apply (ad_SF_compat _ (SF_val_seq f a b n)). by apply SF_sorted_f2, unif_part_sort. rewrite SF_lx_f2 ; replace (head 0 (unif_part a b n) :: behead (unif_part a b n)) with (unif_part a b n) by auto. rewrite -nth_last size_mkseq nth_mkseq ?S_INR //= ; field ; apply Rgt_not_eq, INRp1_pos. now rewrite size_mkseq ; apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy