proposition: Lemma ex_maxset P : (exists A, P A) -> {A | maxset P A}.
proof: Proof. move=> exP; have{exP}: exists A, P (~: A). by case: exP => A PA; exists (~: A); rewrite setCK. by case/ex_minset=> A minA; exists (~: A); rewrite /maxset unlock setCK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)