proposition: Lemma setpart_eq P x A B : A \in P -> B \in P -> x \in A -> x \in B -> A = B.
proof: Proof. move=> AinP BinP xinA xinB; apply/eqP. have /contraR := trivIsetP (trivIsetpart P) A B AinP BinP; apply. rewrite -setI_eq0; apply/set0Pn; exists x. by rewrite inE xinA xinB. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition