proposition: Lemma partitions_piP p E f: inc f (partitions_pi p E) <-> partition_with_pi_elements p E f.
proof: Proof. split; first by case /Zo_P. move=> h; apply: Zo_i =>//. move: h => [p2 _ [p5 _ p7]]. set (g := triple (domain p) (\Po E) f). have ->: (domain p = source g) by rewrite /g -p2; aw. have ->: (\Po E = target g) by rewrite /g; aw. have ->: (f = graph g) by rewrite /g; aw. apply: gfunctions_i; apply: function_pr =>// t. move/(range_gP p5) => [x xdf ->]; apply /setP_P. move => y; rewrite -p7 => hh; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)