proposition: Lemma maxset_exists (P : pred {set A}) C : P C -> {F | maxset P F & C \subset F}.
proof: Proof. move=> PC. have{PC}: exists A, P A && (C \subset A). by exists C; rewrite PC /=. case/ex_maxset => B. move/maxsetP => []. case/andP => BP CB maxB. exists B => //. apply/maxsetP. split=> // D PD BD. rewrite (maxB D) // PD. by rewrite (subset_trans CB). Qed.
imports: mathcomp(all_ssreflect)