proposition: Lemma mclosure_mrank s : mrank (mclosure s) = mrank s.
proof: Proof. have := mrank_subset (mclosure_sub s). rewrite leq_eqVlt => /orP[/eqP<-//|sLcls]. have [s1 [rs1E s1IM s1Ss]] := mrankE s. have [s2 [rs2E s2IM s2Ss]] := mrankE (cl s). case: (msets_card s1IM s2IM); first by rewrite rs1E rs2E. move=> x; rewrite inE => /andP[xNIs1 xIs2] xs1IM. have /(leq_mrank xs1IM) : x |: s1 \subset x |: s by apply: setUS. rewrite cardsU1 xNIs1. have: x \in mclosure s by apply: (subsetP s2Ss). by rewrite inE => /eqP->; rewrite add1n -rs1E ltnn. Qed.
imports: mathcomp(all_ssreflect)