proposition: Lemma sorted_leq_nth_in x0 s : all P s -> sorted leT s -> {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> leT i j}}.
proof: Proof. move=> Ps s_sorted x y xs ys; rewrite leq_eqVlt=> /predU1P[->|]. exact/leT_refl/all_nthP. exact: sorted_ltn_nth_in. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)