proposition: Lemma mcoverI s s1 s2 : mcover s1 s -> mcover s2 s -> s1 != s2 -> s1 :&: s2 = s.
proof: Proof. move=> /mcoverP[s1F sF sPs1 s1Min] /mcoverP[s2F _ sPs2 s2Min] s1Ds2. have s1s2F : s1 :&: s2 \in mflats by apply: mflats_setI. case: (s1Min _ s1s2F)=> // [||s1s2E1]; first by rewrite subsetI !proper_sub. by apply: subsetIl. case: (s2Min _ s1s2F)=> // [||s1s2E2]; first by rewrite subsetI !proper_sub. by apply: subsetIr. by case/eqP: s1Ds2; rewrite -s1s2E1. Qed.
imports: mathcomp(all_ssreflect)