proposition: Lemma le_sorted_leq_nth (x0 : T) (s : seq T) : sorted <=%O s -> {in [pred n | (n < size s)%N] &, {homo nth x0 s : i j / (i <= j)%N >-> i <= j}}.
proof: Proof. exact/sorted_leq_nth/le_refl/le_trans. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)