proposition: Lemma SF_inf_fun_rw (f : R -> R) (a b : R) (n : nat) (x : R) (Hx : a <= x <= b) : SF_inf_fun f a b n x = match (unif_part_nat a b n x Hx) with | inleft H => Inf_fct f (nth 0 (unif_part a b n) (proj1_sig H)) (nth 0 (unif_part a b n) (S (proj1_sig H))) | inright _ => Inf_fct f (nth 0 (unif_part a b n) (n)) (nth 0 (unif_part a b n) (S n)) end.
proof: Proof. have Hab : (a <= b) ; [by apply Rle_trans with (1 := proj1 Hx), Hx | ]. rewrite /SF_inf_fun /SF_inf_seq ; case: Rle_dec => // _. case: unif_part_nat => {Hx} [ [ i [Hx Hi] ] | Hx] ; simpl proj1_sig. case: (unif_part a b n) (unif_part_sort a b n Hab) i Hi x Hx => {a b Hab n} [| h s] Hs /= i Hi. by apply Nat.nlt_0_r in Hi. case: (s) Hs (i) ((proj2 (Nat.succ_lt_mono _ _) Hi)) => {s i Hi} [| h0 s] Hs /= i Hi. by apply Nat.nlt_0_r in Hi. elim: (s) h h0 Hs (i) ((proj2 (Nat.succ_lt_mono _ _) Hi)) => {s i Hi} [|h1 s IH] h h0 Hs /= i Hi x Hx. by apply Nat.nlt_0_r in Hi. case: i Hx Hi => [|i]/= Hx Hi. rewrite /SF_fun /=. case: Rlt_dec => [Hx0 | _ ]. contradict Hx0 ; apply Rle_not_lt, Hx. case: Rlt_dec => // Hx0 ; contradict Hx0 ; apply Hx. rewrite -(IH h0 h1 (proj2 Hs) i ((proj2 (Nat.succ_lt_mono _ _) Hi)) x Hx). rewrite /SF_fun /= ; case: Rlt_dec => [ Hx0 | _ ] //. contradict Hx0 ; apply Rle_not_lt, Rle_trans with (1 := proj1 Hs), Rle_trans with (2 := proj1 Hx), (sorted_head [:: h0, h1 & s] _ (proj2 Hs)) ; simpl; intuition. case: Rlt_dec => [ Hx0 | _ ] //. contradict Hx0 ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hx), (sorted_head [:: h0, h1 & s] _ (proj2 Hs)) ; simpl; intuition. move: x Hx. suff : (1 < size (unif_part a b n))%nat. have: (n = size (unif_part a b n) - 2)%nat ; [ rewrite size_mkseq ; intuition | move => {3 5 8 10}->]. case: (unif_part a b n) (unif_part_sort a b n Hab) => {a b Hab n} [| h s] Hs /= Hi. by apply Nat.nlt_0_r in Hi. case: s h Hs Hi => [| h0 s] h Hs /= Hi. by apply Nat.lt_irrefl in Hi. rewrite Nat.sub_0_r ; elim: s h h0 Hs {Hi} => [| h1 s IH] h h0 Hs /= x Hx. rewrite /SF_fun /= ; case: Rlt_dec => [Hx0 | _]. contradict Hx0 ; apply Rle_not_lt, Hx. case: Rle_dec => [| Hx0] // ; contradict Hx0 ; apply Hx. rewrite -(IH h0 h1 (proj2 Hs) x Hx). rewrite /SF_fun /= ; case: Rlt_dec => [ Hx0 | _ ] //. contradict Hx0 ; apply Rle_not_lt, Rle_trans with (1 := proj1 Hs), Rle_trans with (2 := proj1 Hx), (sorted_head [:: h0, h1 & s] _ (proj2 Hs)) ; simpl; intuition. case: Rlt_dec => [ Hx0 | _ ] //. contradict Hx0 ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hx), (sorted_head [:: h0, h1 & s] _ (proj2 Hs)) ; simpl; intuition. rewrite size_mkseq ; by apply ->Nat.succ_lt_mono; apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy