proposition: Lemma sorted_last (s : seq R) i : sorted Rle s -> (i < size s)%nat -> forall x0, nth x0 s i <= last x0 s.
proof: Proof. move => Hs Hi x0 ; rewrite -nth_last. case: s Hi Hs => [| h s] Hi Hs //. by apply Nat.nlt_0_r in Hi. apply sorted_incr => //. intuition. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy