fact: Definition partition_with_pi_elements p E f := [/\ domain f = domain p, (forall i, inc i (domain p) -> cardinal (Vg f i) = Vg p i) & partition_w_fam f E].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)