fact: Definition join_finer_eq P Q := connect (relU (fun x y => y \in pblock P x) (fun x y => y \in pblock Q x)).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition