proposition: Lemma sorted_dec (s : seq R) x0 (x : R) : sorted Rle s -> head x0 s <= x <= last x0 s -> {i : nat | nth x0 s i <= x < nth x0 s (S i) /\ (S (S i) < size s)%nat} + {nth x0 s (size s - 2)%nat <= x <= nth x0 s (size s - 1)%nat}.
proof: Proof. case: s => [/= _ Hx| h s] ; simpl minus ; rewrite -?Nat.sub_0_r. by right. case: s => [/= _ Hx| h0 s] ; simpl minus ; rewrite -?Nat.sub_0_r. by right. elim: s h h0 => [/= | h1 s IH] h h0 Hs Hx. by right. case: (Rlt_le_dec x h0) => Hx'. left ; exists O => /= ; intuition. case: (IH h0 h1) => [ | |[i Hi]|Hi]. apply Hs. split ; [apply Hx'|apply Hx]. left ; exists (S i) => /= ; intuition. right => /= ; simpl in Hi. by rewrite Nat.sub_0_r in Hi. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy