proposition: Lemma ex_max X : X `<=` U -> P X -> exists M, [/\ X `<=` M , M `<=` U & maximal M].
proof: Proof. move: X. apply: slack_ind => X IH inU pX. case/boolP :(maximalb X) => [/maximalP|]; first by exists X; rewrite subxx. rewrite negb_and pX. case/allPn => Y. rewrite powersetE negb_imply negbK => H1 /andP [H2 pY]. case: (IH _ H1 H2 pY) => M [YM MU Hm]. exists M. split => //. apply: (sub_trans _ YM). exact: properW. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)