proposition: Lemma leq_size_uniq s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> uniq s2.
proof: Proof. elim: s1 s2 => [[] | x s1 IHs s2] // Us1x; have /andP[not_s1x Us1] := Us1x. case/forall_cons => /rot_to[i s3 def_s2] ss12 le_s21. rewrite -(rot_uniq i) -(size_rot i) def_s2 /= in le_s21 *. have ss13 y (s1y : y \in s1): y \in s3. by have:= ss12 y s1y; rewrite -(mem_rot i) def_s2 inE (negPf (memPn _ y s1y)). rewrite IHs // andbT; apply: contraL _ le_s21 => s3x; rewrite -leqNgt. by apply/(uniq_leq_size Us1x)/allP; rewrite /= s3x; apply/allP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)