proposition: Lemma card_partitions3 p E f g: partition_with_pi_elements p E f -> inc g (permutations E) -> inc (partitions_aux f g) (partitions_pi p E).
proof: Proof. move=> pip gp. apply /partitions_piP. move: gp => /Zo_P [/functionsP [fg sg tg [ig sjg]]]. have Ha:forall u, inc u (domain f) -> sub (Vg f u) (source g). rewrite sg; apply: (pip_prop0 pip). move: pip => [df cVg [fgf duj ue]]. hnf; rewrite / partitions_aux; saw. rewrite df;move=> i idp; rewrite LgV //- (cVg _ idp) ; symmetry. apply /card_eqP/Eq_restriction1 =>//; apply: Ha =>//; ue. split;fprops. apply: mutually_disjoint_prop=>//; aw => i j y idp jdp; rewrite !LgV//. move: (Ha _ idp) (Ha _ jdp)=> s1 s2. move=> /(Vf_image_P fg s1) [u ui Wu] /(Vf_image_P fg s2) [v vi Wv]. have uv: u = v. move: ig => [_ ig]; rewrite Wv in Wu;apply: ig; fprops. case: (duj _ _ idp jdp) => //; rewrite /disjoint => ns. rewrite -uv in vi; empty_tac1 u. rewrite -tg;set_extens x. move /setUb_P1 => [y ydp]. move /(Vf_image_P fg (Ha _ ydp)) => [u ua ->]; Wtac; exact: (Ha _ ydp). move=> xtg; move: ((proj2 sjg) _ xtg)=> [y ysf Wy]. move: ysf; rewrite sg -ue;move=> /setUb_P [t tf etc]. apply /setUb_P1; ex_tac; apply /(Vf_image_P fg (Ha _ tf)); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)