proposition: Lemma sorted_incr (s : seq R) i j : sorted Rle s -> (i <= j)%nat -> (j < size s)%nat -> forall x0, nth x0 s i <= nth x0 s j.
proof: Proof. elim: i j s => [| i IH] j s Hs Hij Hj x0. rewrite nth0 ; by apply sorted_head. case: j Hij Hj => [| j] Hij Hj. by apply Nat.nle_succ_0 in Hij. case: s Hs Hj => [| h s] Hs Hj. by apply Nat.nlt_0_r in Hj. apply (IH j s) with (x0 := x0) => //. case: (s) Hs => {s Hj} [| h0 s] Hs ; apply Hs. apply le_S_n, Hij. apply le_S_n, Hj. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy