proposition: Lemma ex_maxset (P : pred {set A}): (exists E, P E) -> {E | maxset P E}.
proof: Proof. move=> exQ. pose pS n := [pred F | P F & #|F| == n]. pose p n := ~~ pred0b (pS n). have {exQ} : exists n, p n. case: exQ => E QE. exists #| E |. rewrite /p. apply/existsP. exists E. by rewrite eqxx andbT. case/(@ex_maxnP _ #|A|). move=> o pi. case/existsP : pi => B /andP [] QB /eqP <-. by apply max_card. move=> i. move/pred0P. case: (pickP (pS i)) => // F. move=> pSF H Hi. exists F. apply/(@maxsetP P). split. rewrite /pS inE in pSF. by case/andP : pSF. move=> G QG FG. apply/eqP. rewrite eqEcard FG /=. move: (Hi #|G|). rewrite /pS inE in pSF. case/andP : pSF => H1 H2. rewrite (eqP H2). apply. apply/existsP. exists G. by rewrite QG eqxx. Qed.
imports: mathcomp(all_ssreflect)