proposition: Lemma mcoverP s1 s2 : reflect [/\ s1 \in mflats, s2 \in mflats, s2 \proper s1 & forall s, s \in mflats -> s2 \subset s -> s \subset s1 -> (s = s1) \/ (s = s2)] (mcover s1 s2).
proof: Proof. apply: (iffP and4P) => [] [H1 H2 H3 H4]; split => //. move=> s V1 V2 V3. have /forallP/(_ s)/implyP H5 := H4. have [] := orP (H5 _) => [|/eqP->|/eqP->] //. - by rewrite V1 V2. - by left. by right. apply/forallP=> s; apply/implyP => /and3P[V1 V2 V3]. by case: (H4 _ V1 V2 V3) => ->; rewrite eqxx // orbT. Qed.
imports: mathcomp(all_ssreflect)