proposition: Lemma triv_part P X : X \in P -> partition P X -> P = [set X].
proof: Proof. Proof using. move=> XinP /and3P[/eqP Hcov /trivIsetP/=/(_ X _ XinP) H H0]. apply/setP=> /= Y; rewrite inE eq_sym; apply/idP/idP=> [YinP | /eqP <- //]. move/(_ Y YinP): H => /contraR; apply. apply/contra: H0; rewrite disjoint_sym -{}Hcov=> /bigcup_disjointP/(_ _ YinP). by move/disjoint_setI0; rewrite setIid => <-. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)