proposition: Lemma uniq_size_uniq s1 s2 : uniq s1 -> s1 =i s2 -> uniq s2 = (size s2 == size s1).
proof: Proof. move=> Us1 eqs12; apply/idP/idP=> [Us2 | /eqP eq_sz12]. by rewrite eqn_leq !uniq_leq_size // => y; rewrite eqs12. by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)