proposition: Lemma maximalP M : reflect (maximal M) (maximalb M).
proof: Proof. apply: (iffP andP) => [[H1 /all_subP H2]|[H1 H2]]; split => //. - move => Y inU. apply/implyP. exact: H2. - apply/all_subP => Y inU. apply/implyP. exact: H2. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)