proposition: Lemma mcover_sub_ex s1 s2 : s1 \in mflats -> s2 \in mflats -> s1 \proper s2 -> exists2 s, mcover s s1 & s \subset s2.
proof: Proof. move=> s1F. elim: {s2}_.+1 {-2}s2 (ltnSn #|s2|) => // n IH s2 s2Ln s2F s1Ps2. have [s2Cs1|] := boolP (mcover s2 s1). by exists s2 => //; case/andP: s1Ps2. rewrite [in X in X -> _]/mcover s1F s2F s1Ps2 negb_forall => /existsP[s3]. rewrite negb_imply negb_or => /and3P[/and3P[s3F s1Ss3 s3Ss2] s3Ds2 s3Ds1]. have [|||s sCs1 sSs3] := IH s3 => //. - have /proper_card/leq_trans->// : s3 \proper s2 by rewrite properEneq s3Ds2. - by rewrite properEneq eq_sym s3Ds1. by exists s => //; apply: subset_trans sSs3 _. Qed.
imports: mathcomp(all_ssreflect)