fact: Definition join_finer P Q := SetPart (equivalence_partitionP (join_finer_equivalence P Q)).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition