proposition: Lemma mcoverPU s1 s2 : s2 \in mflats -> reflect (exists2 a, a \notin s2 & s1 = mclosure (a |: s2)) (mcover s1 s2).
proof: Proof. move=> s2F. apply: (iffP idP)=> [|[a aNIs2->]]; first by apply: mcoverE. by apply: mcover_mclosure. Qed.
imports: mathcomp(all_ssreflect)