proposition: Lemma sorted_ltn_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. by move=> Ps; rewrite sorted_pairwise_in //; apply/pairwiseP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)