proposition: Lemma mclosure_ex a b s : b \in (mclosure (a |: s) :\: mclosure s) -> a \in (mclosure (b |: s) :\: mclosure s).
proof: Proof. rewrite inE => /andP[bNIs bIas]. have [/mclosureU1 asE|aNIs] := boolP (a \in mclosure s). by case/negP: bNIs; rewrite -asE. rewrite inE aNIs /=. move: bIas; rewrite !inE setUCA => /eqP->. by rewrite !mrank_setU1. Qed.
imports: mathcomp(all_ssreflect)