proposition: Lemma uniq_leq_size s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s1 <= size s2.
proof: Proof. elim: s1 s2 => //= x s1 IHs s2 /andP[not_s1x Us1] /forall_cons[s2x ss12]. have [i s3 def_s2] := rot_to s2x; rewrite -(size_rot i s2) def_s2. apply: IHs => // y s1y; have:= ss12 y s1y. by rewrite -(mem_rot i) def_s2 inE (negPf (memPn _ y s1y)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)