proposition: Lemma maxset_exists P C : P C -> {A : sT | maxset P A & C \subset A}.
proof: Proof. move=> PC; pose P' B := P (~: B); have: P' (~: C) by rewrite /P' setCK. case/minset_exists=> B; rewrite -[B]setCK setCS. by exists (~: B); rewrite // /maxset unlock. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)