proposition: Lemma sorted_uniq_in s : {in s & &, transitive leT} -> {in s, irreflexive leT} -> sorted leT s -> uniq s.
proof: Proof. move=> /in3_sig leT_tr /in1_sig leT_irr; case/all_sigP: (allss s) => s' ->. by rewrite sorted_map (map_inj_uniq val_inj); exact: sorted_uniq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)