proposition: Lemma mclosureU1 a s : a \in mclosure s -> mclosure (a |: s) = mclosure s.
proof: Proof. rewrite inE => /eqP aIs; apply/eqP. rewrite eqEsubset andbC mclosure_subset ?subsetUr //=. apply/subsetP=> b; rewrite !inE => /eqP bIas. rewrite eqn_leq andbC mrank_subset ?subsetUr //=. by rewrite -aIs -bIas mrank_subset // setUCA subsetUr. Qed.
imports: mathcomp(all_ssreflect)