proposition: Lemma sorted_leq_last s : sorted leq s -> forall i, i \in s -> i <= last 0 s.
proof: Proof. move=> H /= i; case/(nthP O) => {}i Hi <-; rewrite -nth_last. case/boolP : (i == (size s).-1) => [/eqP <- //|si]. apply (sorted_ltn_nth leq_trans) => //. by rewrite inE prednK // (leq_trans _ Hi). by rewrite ltn_neqAle si /= -ltnS prednK // (leq_trans _ Hi). Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext