proposition: Lemma uniq_min_size s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> (size s1 = size s2) * (s1 =i s2).
proof: Proof. move=> Us1 ss12 le_s21; have Us2: uniq s2 := leq_size_uniq Us1 ss12 le_s21. suffices: s1 =i s2 by split; first by apply/eqP; rewrite -uniq_size_uniq. move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x. rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //. by apply/allP; rewrite /= s2x; apply/allP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)