proposition: Lemma pip_prop0 p E f: partition_with_pi_elements p E f -> forall i, inc i (domain f) -> sub (Vg f i) E.
proof: Proof. move=> [df cVg [fgf duj ue]]. move=>i idp t tW; rewrite -ue; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)