proposition: Lemma maxset_is_unique E : is_unique (maxset E) (fun E' => E' \subset E /\ covered_by E E' /\ P E').
proof: Proof. rewrite /is_unique => E'. case=> EsubE'. case=> EE' HE'. apply/setP => /= n0. case/boolP : (n0 \in maxset E) => Hn0. move/forallP : EE'. move=> /(_ (maxset E)). move /implyP. move/(_ (maxset_in_Psets E)). move /subsetP. by apply. apply: contraTF Hn0. rewrite negbK => n0E'. apply/bigcupP => /=. exists E' => //. by rewrite inE HE' andbT. Qed.
imports: mathcomp(all_ssreflect)