proposition: Lemma SF_fun_incr (s : SF_seq) (y0 : T) (x : R) Hs Hx : SF_fun s y0 x = match (sorted_dec (SF_lx s) 0 x Hs Hx) with | inleft H => nth y0 (SF_ly s) (proj1_sig H) | inright _ => nth y0 (SF_ly s) (SF_size s -1)%nat end.
proof: Proof. rewrite /SF_fun /=. move: Hs Hx ; apply SF_cons_dec with (s := s) => {s} [/= x1 | h s] Hs /= Hx. case: sorted_dec => /= [[i Hi]|Hi] ; rewrite /SF_ly ; case: Rle_dec => //= ; case: i Hi => //. case: Rlt_dec => [Hx' | _]. contradict Hx' ; apply Rle_not_lt, Hx. move: h Hs Hx ; apply SF_cons_ind with (s := s) => {s} [x1 | h0 s IH] h Hs /= Hx. case: sorted_dec => [/= [i [Hi' Hi]] /= |Hi]. by apply Nat.succ_lt_mono, Nat.succ_lt_mono, Nat.nlt_0_r in Hi. case: Hx => Hx Hx' ; apply Rle_not_lt in Hx ; case: Rle_dec => //. case: Rlt_dec => Hx'. case: sorted_dec => /= [[i Hi]|Hi]/=. case: i Hi => //= i Hi ; contradict Hx' ; apply Rle_not_lt, Rle_trans with (2 := proj1 (proj1 Hi)). simpl in Hs ; elim: (unzip1 (SF_t s)) (fst h0) (SF_h s) (i) (proj2 Hs) (proj2 Hi) => {s IH Hs Hx Hi h h0} [| h1 s IH] h h0 n Hs Hn. repeat apply <-Nat.succ_lt_mono in Hn ; by apply Nat.nlt_0_r in Hn. case: n Hn => [| n] Hn. apply Rle_refl. apply Rle_trans with (1 := proj1 Hs) => //= ; intuition. contradict Hx' ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hi). simpl in Hs ; elim: (unzip1 (SF_t s)) (fst h0) (SF_h s) (proj2 Hs) => {s IH Hs Hx Hi h h0} [| h1 s IH] h h0 Hs. apply Rle_refl. apply Rle_trans with (1 := proj1 Hs) => //= ; intuition. have : fst h0 <= x <= last (SF_h s) (unzip1 (SF_t s)) => [ | {} Hx']. split ; [by apply Rnot_lt_le | by apply Hx]. rewrite (IH h0 (proj2 Hs) Hx') => {IH} ; case: sorted_dec => [[i [Hxi Hi]]|Hi] ; case: sorted_dec => [[j [Hxj Hj]]|Hj] ; rewrite ?Nat.sub_0_r //=. move : h h0 i j Hs {Hx Hx'} Hxi Hi Hxj Hj ; apply SF_cons_ind with (s := s) => {s} [x1 | h1 s IH] h h0 i j Hs //= Hxi Hi Hxj Hj. by apply Nat.succ_lt_mono, Nat.succ_lt_mono, Nat.nlt_0_r in Hi. case: j Hxj Hj => [/= | j] Hxj Hj. case: Hxj => _ Hxj ; contradict Hxj ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hxi). elim: (i) Hi => {i Hxi IH} //= [| i IH] Hi. apply Rle_refl. apply Rle_trans with (1 := IH (Nat.lt_trans _ _ _ (Nat.lt_succ_diag_r _) Hi)), (sorted_nth Rle) ; [apply Hs | simpl ; intuition]. case: i Hxi Hi => [/= | i] Hxi Hi. case: j Hxj Hj => [//= | j] Hxj Hj. case: Hxi => _ Hxi ; contradict Hxi ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hxj) ; elim: (j) Hj => {j Hxj IH} //= [| j IH] Hj. apply Rle_refl. apply Rle_trans with (1 := IH (Nat.lt_trans _ _ _ (Nat.lt_succ_diag_r _) Hj)), (sorted_nth Rle) ; [apply Hs | simpl ; intuition]. apply (IH h0 h1 i j) => //. apply Hs. apply Nat.succ_lt_mono, Hi. apply Nat.succ_lt_mono, Hj. simpl in Hxi, Hj ; case: Hxi => _ Hxi ; contradict Hxi ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hj). move: Hi Hs ; rewrite ?SF_lx_cons /SF_lx. elim: i (fst h) (fst h0) (SF_h s) (unzip1 (SF_t s)) => {s Hx Hx' Hj h y0 h0} [| i IH] h h0 h1 s Hi Hs. case: s Hi Hs => [| h2 s] Hi Hs /=. by apply Nat.succ_lt_mono, Nat.succ_lt_mono, Nat.nlt_0_r in Hi. elim: s h h0 h1 h2 {Hi} Hs => [| h3 s IH] h h0 h1 h2 Hs /=. apply Rle_refl. apply Rle_trans with (r2 := h2). apply Hs. apply (IH h0 h1). apply (proj2 Hs). case: s Hi Hs => [| h2 s] Hi Hs. by apply Nat.succ_lt_mono, Nat.succ_lt_mono, Nat.nlt_0_r in Hi. apply (IH h0 h1 h2 s). apply Nat.succ_lt_mono, Hi. apply Hs. simpl in Hxj, Hi ; case: Hxj => _ Hxj ; contradict Hxj ; apply Rle_not_lt, Rle_trans with (2 := proj1 Hi). move: Hj Hs ; rewrite ?SF_lx_cons /SF_lx. rewrite Nat.sub_0_r ; elim: j (fst h) (fst h0) (SF_h s) (unzip1 (SF_t s)) => {s Hx Hx' Hi h y0 h0} [ | j IH] h h0 h1 s Hj Hs /=. elim: s h h0 h1 {Hj} Hs => [| h2 s IH] h h0 h1 Hs /=. apply Rle_refl. apply Rle_trans with (r2 := h1). apply Hs. apply (IH h0 h1 h2). apply (proj2 Hs). case: s Hj Hs => [| h2 s] Hj Hs. by apply Nat.succ_lt_mono, Nat.succ_lt_mono, Nat.succ_lt_mono, Nat.nlt_0_r in Hj. apply (IH h0 h1 h2 s). apply Nat.succ_lt_mono, Hj. apply Hs. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy