proposition: Lemma sorted_leq_nth x0 s : sorted leT s -> {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> leT i j}}.
proof: Proof. exact/sorted_leq_nth_in/all_predT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)