proposition: Lemma msets_card s1 s2 : s1 \in msets M -> s2 \in msets M -> #|s1| < #|s2| -> exists2 x, x \in s2 :\: s1 & (x |: s1) \in msets M.
proof: Proof. move=> s1IM s2IM s1Ls2. have /and3P[_ _ /forallP/(_ s1)/forallP/(_ s2) H] := wf_msets M. have /implyP := H. rewrite s1IM s2IM => /(_ s1Ls2) /existsP[x /andP[Hx1 Hx2]]. by exists x. Qed.
imports: mathcomp(all_ssreflect)