proposition: Lemma maxsetP (P : {set A} -> bool) E : reflect ((P E) /\ (forall F, P F -> E \subset F -> E = F)) (maxset P E).
proof: Proof. case H : (maxset P E); [apply ReflectT | apply ReflectF]. case/andP : H => -> /forallP H. split => // F H1 H2. move: (H F). by rewrite H1 H2 /= eq_sym eqb_id => /eqP. case => H1 H2. move/negP : H; apply. rewrite /maxset H1 /=. apply/forallP => F. case H : (_ && _). case/andP : H. move/H2 => H3; move/H3 => ->. by rewrite eqxx. rewrite eq_sym. rewrite eqbF_neg. apply/eqP => ?; subst F. rewrite H1 /= in H. move/negP : H; by apply. Qed.
imports: mathcomp(all_ssreflect)