proposition: Lemma mrank_setU1 a s : a \notin mclosure s -> mrank (a |: s) = (mrank s).+1.
proof: Proof. rewrite inE => aIs; have := mrank_mod [set a] s. have-> :[set a] :&: s = set0. apply/setP=> y; rewrite !inE; case: eqP => // -> /=. apply/idP => Ha; case/eqP: aIs. by congr mrank; apply/setUidPr; rewrite sub1set. rewrite mrank_set0 addn0. case: mrank (mrank_set1 a) => [_ asLs|[_|]//]. case/negP: aIs. by rewrite eqn_leq andbC mrank_subset ?subsetUr. rewrite leq_eqVlt => /orP[/eqP//|asLs]. case/negP: aIs. by rewrite eqn_leq andbC mrank_subset ?subsetUr. Qed.
imports: mathcomp(all_ssreflect)