proposition: Lemma perm_size_uniq (T : eqType) (s1 s2 : seq T) : uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> perm_eq s1 s2.
proof: Proof. move=> Hus1 Hsubs /(uniq_min_size Hus1 Hsubs) => [][Hsz Heq]. apply: (uniq_perm Hus1); last exact Heq. by rewrite -(eq_uniq Hsz Heq). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp