proposition: Lemma mcoverE s1 s2 : mcover s1 s2 -> exists2 a, a \notin s2 & s1 = mclosure (a |: s2).
proof: Proof. move=> /mcoverP[s1F s2F s2Ps1 HS]. have /properP[s2Ss1 [a aIs1 aNIs2]] := s2Ps1. exists a => //. case (HS (mclosure (a |: s2))) => //. - by apply: mclosure_mflats. - apply: subset_trans (subsetUr _ _) (mclosure_sub _). - rewrite -(mflats_mclosure s1F). apply: mclosure_subset. by rewrite subUset sub1set aIs1. move=> /setP/(_ a). by rewrite (subsetP (mclosure_sub _)) ?(negPf aNIs2) // !inE eqxx. Qed.
imports: mathcomp(all_ssreflect)