proposition: Lemma sorted_head (s : seq R) i : sorted Rle s -> (i < size s)%nat -> forall x0, head x0 s <= nth x0 s i.
proof: Proof. case: s => [| h s]. move => _ Hi ; by apply Nat.nlt_0_r in Hi. elim: s h i => [| h0 s IH] h i Hs Hi x0. apply Nat.lt_succ_r, Nat.le_0_r in Hi ; rewrite Hi ; apply Rle_refl. case: i Hi => [| i] Hi. apply Rle_refl. apply Rle_trans with (r2 := head x0 (h0::s)). apply Hs. apply IH. apply Hs. apply ->Nat.lt_succ_r; now apply Hi. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy