proposition: Lemma setpart_conn P : connect_sym (fun x y : T => y \in (pblock P x)).
proof: Proof. suff impl x y : x \in pblock P y -> y \in pblock P x. by apply: sym_connect_sym=> x y; apply/idP/idP; apply impl. move=> /[dup] /(same_pblock (trivIsetpart P)) peq. rewrite -peq mem_pblock=> /pblock_mem; rewrite {x}peq. by rewrite mem_pblock pblock_in. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition