proposition: Lemma lt_sorted_uniq_le s : sorted <%O s = uniq s && sorted <=%O s.
proof: Proof. rewrite le_sorted_pairwise lt_sorted_pairwise uniq_pairwise -pairwise_relI. by apply/eq_pairwise => ? ?; rewrite lt_neqAle. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)