proposition: Lemma maxset_in_Psets E : maxset E \in Psets E.
proof: Proof. rewrite /Psets inE maxset_is_subset /= /maxset. suff Hgen : forall F : {set {set A}} , (forall s', s' \in F -> P s') -> P (\bigcup_(s in F) s). apply Hgen => s'. rewrite inE. by case/andP. move=> F /= HF. move Hk : (#| F |) => k. elim: k => [ | k IH ] in F Hk HF *. rewrite big_pred0. by rewrite P0. move=> s /=. apply/negbTE. move/eqP : Hk. rewrite cards_eq0 => /negPn. apply: contra => sF. apply/set0Pn; by exists s. have : #|F| != O by rewrite Hk. rewrite cards_eq0. case/set0Pn => f0 Hf0. rewrite -(@setD1K _ f0 F) // bigcup_setU PU //. rewrite (big_pred1 f0). by apply HF. move=> /= s; by rewrite inE. apply IH. rewrite (cardsD1 f0) in Hk. rewrite Hf0 in Hk. rewrite add1n in Hk. by case: Hk. move=> s' Hs'. apply HF. rewrite inE in Hs'. by case/andP : Hs'. Qed.
imports: mathcomp(all_ssreflect)