proposition: Lemma mclosure_subset s1 s2 : s1 \subset s2 -> mclosure s1 \subset mclosure s2.
proof: Proof. move=> s1Ss2; apply/subsetP=> x; rewrite !inE => /eqP rxs1E. rewrite eqn_leq [_ <= mrank (_ |: _)]mrank_subset ?andbT; last first. by apply: subsetUr. have->: x |: s2 = (x |: s1) :|: s2. rewrite -setUA; congr (_ |: _). by apply/sym_equal/setUidPr. rewrite -(leq_add2r (mrank ((x |: s1) :&: s2))) (addnC (mrank s2)). suff mrE : mrank ((x |: s1) :&: s2) = mrank (x |: s1). by rewrite [X in _ <= X + _]mrE; apply: mrank_mod. have [xIs2|xNIs2] := boolP (x \in s2). congr mrank; apply/setIidPl. by rewrite subUset /= sub1set xIs2. rewrite rxs1E setIUl (_ : _ :&: _ = set0) ?set0U. by congr mrank; apply/setIidPl. apply/setP=> y; rewrite !inE; case: eqP => [->|] //. by rewrite (negPf xNIs2). Qed.
imports: mathcomp(all_ssreflect)