proposition: Lemma mcover_mclosure a s1 : s1 \in mflats -> a \notin s1 -> mcover (mclosure (a |: s1)) s1.
proof: Proof. move=> s1F aNIs1. have [|s sCs1 s1Sas1] := mcover_sub_ex s1F (mclosure_mflats (a |: s1)). rewrite properE (subset_trans _ (mclosure_sub _)) ?subsetUr //=. apply/negP=> /subsetP/(_ a). rewrite (negPf aNIs1) (subsetP (mclosure_sub _)). by move=> /(_ isT). by rewrite !inE eqxx. have [b bNIs1 sE] := mcoverE sCs1. suff/eqP->: cl(a |: s1) == cl(b |: s1) by rewrite -sE. rewrite eqEsubset; apply/andP; split; last first. by rewrite -sE (subset_trans _ s1Sas1). rewrite -(mclosure_invo (b |: _)) mclosure_subset //. rewrite subUset sub1set -[in X in _ && (X \subset _)](mflats_mclosure s1F). rewrite mclosure_subset ?andbT ?subsetUr //. suff : a \in (mclosure (b |: s1) :\: mclosure s1) by rewrite inE => /andP[]. apply: mclosure_ex. rewrite inE mflats_mclosure // bNIs1 (subsetP s1Sas1) // sE. by rewrite (subsetP (mclosure_sub _)) // !inE eqxx. Qed.
imports: mathcomp(all_ssreflect)