proposition: Lemma ad_SF_compat z0 (s : SF_seq) (pr : SF_sorted Rle s) : adapted_couple (SF_fun s z0) (head 0 (SF_lx s)) (last 0 (SF_lx s)) (SF_lx s) (SF_ly s).
proof: Proof. have H : ((head 0 (SF_lx s)) <= (last 0 (SF_lx s))). move: pr ; rewrite /SF_sorted. case: (SF_lx s) => {s} [| h s] Hs. apply Rle_refl. rewrite -nth0 ; apply sorted_last => // ; apply Nat.lt_0_succ. rewrite /adapted_couple ?nth_compat ?size_compat ?nth0 ?nth_last /Rmin /Rmax ?SF_size_lx ?SF_size_ly ; case: (Rle_dec (head 0 (SF_lx s)) (last 0 (SF_lx s))) => // {H} _ ; intuition. apply sorted_compat => //. move: i pr H ; apply SF_cons_dec with (s := s) => {s} [x0 | h s] i Hs Hi x [Hx0 Hx1]. by apply Nat.nlt_0_r in Hi. rewrite /SF_fun ?SF_size_cons ?nth_compat -?SF_size_lx ?SF_lx_cons in Hi, Hx0, Hx1 |- *. simpl. move: h i x {1}z0 Hs Hi Hx0 Hx1 ; apply SF_cons_ind with (s := s) => {s} [x1 | h0 s IH] h ; case => [| i ] x z0' Hs Hi Hx0 Hx1 //= ; case: Rlt_dec => Hx' //. now contradict Hx' ; apply Rle_not_lt, Rlt_le, Hx0. now case: Rle_dec => Hx'' // ; contradict Hx'' ; apply Rlt_le, Hx1. now rewrite /= in Hi ; by apply Nat.succ_lt_mono, Nat.nlt_0_r in Hi. now rewrite /= in Hi ; by apply Nat.succ_lt_mono, Nat.nlt_0_r in Hi. now contradict Hx' ; apply Rle_not_lt, Rlt_le, Hx0. now case: Rlt_dec => Hx'' //. now contradict Hx' ; apply Rle_not_lt, Rlt_le, Rle_lt_trans with (2 := Hx0) ; have Hi' : (S i < size (SF_lx (SF_cons h (SF_cons h0 s))))%nat ; [ rewrite ?SF_lx_cons /= in Hi |-* ; apply Nat.lt_trans with (1 := Hi), Nat.lt_succ_diag_r | ] ; apply (sorted_head (SF_lx (SF_cons h (SF_cons h0 s))) (S i) Hs Hi' 0). rewrite -(IH h0 i x (snd h)) //=. apply Hs. rewrite ?SF_lx_cons /= in Hi |-* ; apply Nat.succ_lt_mono, Hi. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy