fact: Definition map_finer A : {set T} := if (boolP (A \in P)) is AltTrue pin then let: exist2 B _ _ := sig2W (is_finerP P Q finPQ A pin) in B else set0.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition