proposition: Lemma mflats_partition s : s \in mflats -> partition [set (s1 :\: s) | s1 in {set M} & mcover s1 s] (~: s).
proof: Proof. move=> sF. apply/and3P; split. - apply/eqP/setP => x; rewrite inE. have [xIs/= |xNIs/=] := boolP (x \in s); apply/idP. move=> /bigcupP/= [s1] /imsetP/= [s2 _ ->]. by rewrite inE xIs. apply/bigcupP; exists (mclosure (x |: s) :\:s). apply/imsetP; exists (mclosure (x |: s)) => //. by rewrite inE mcover_mclosure. by rewrite inE xNIs (subsetP (mclosure_sub _)) // !inE eqxx. - apply/trivIsetP=> /= s1 s2 /imsetP/= [s3]. rewrite inE => s3Cs -> /imsetP/= [s4]. rewrite inE => s4Cs -> s3Ds4. rewrite -setI_eq0 -setDIl (mcoverI s3Cs) ?setDv //. by apply: contra s3Ds4 => /eqP->. apply/imsetP=> /= [] [s1]. rewrite inE => /and4P[_ _ sPs1 _] /eqP. rewrite eq_sym setD_eq0 => s1Ss. case/negP : (proper_neq sPs1). by rewrite eqEsubset s1Ss proper_sub. Qed.
imports: mathcomp(all_ssreflect)