proposition: Lemma mrank_compl s1 s2 : s1 \in msets M -> s1 \subset s2 -> exists2 s3 : {set M}, s1 \subset s3 & is_rset s3 s2.
proof: Proof. elim: {s1}_.+1 {-2}s1 (ltnSn (#|s2 :\: s1|)) => // n IH s1 s1Ds2 s1IM s1Ss2. have [s3 [Rs3 s3IM s3Ss2]] := mrankE s2. have := leq_mrank s1IM s1Ss2. rewrite -Rs3 leq_eqVlt => /orP[/eqP s1Es3|s1Ls3]. by exists s1 => //; split => //; rewrite s1Es3. have [x xIs3s1 xs1IM] := msets_card s1IM s3IM s1Ls3. case: (IH (x |: s1)) => // [||s4 s4IM s4rS]. - move: xIs3s1; rewrite in_setD => /andP[xNIs1 xIs3]. move : s1Ds2; rewrite (cardsD1 x) setDDl setUC in_setD xNIs1 /=. by rewrite (subsetP s3Ss2) //= ltnS. - rewrite subUset s1Ss2 andbT sub1set. apply: (subsetP (_ : s3 :\: s1 \subset s2)) => //. by apply: subset_trans (subsetDl _ _) _. exists s4 => //. by apply: subset_trans (subsetUr _ _) s4IM. Qed.
imports: mathcomp(all_ssreflect)