proposition: Lemma sorted_pairwise_in s : all P s -> sorted leT s = pairwise leT s.
proof: Proof. by elim: s => //= x s IHs /andP [Px Ps]; rewrite path_sorted_inE ?IHs //= Px. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)