proposition: Lemma card_partitions5P p E f g h: finite_int_fam p -> csum p = cardinal E -> partition_with_pi_elements p E f -> inc h (permutations E) -> inc g (permutations E) -> ( (partitions_aux f g = partitions_aux f h) <-> (forall i, inc i (domain p) -> Vfs ( (inverse_fun h) \co g) (Vg f i) = (Vg f i))).
proof: Proof. move=> fip spE pip; move: (pip_prop0 pip)=> Ht. move: pip => [df cVg [fgf duj ue]]. move => /Zo_P [] /functionsP [fh sh th] [inh [_ sjh]]. move => /Zo_P [] /functionsP [fg sg tg] bg. have fih: function (inverse_fun h) by apply: bijective_inv_f. have cih: (inverse_fun h) \coP g by saw; ue. have fcih : function ((inverse_fun h) \co g) by fct_tac. rewrite -df; split. move=> eq i idp; move: (f_equal (Vg ^~ i) eq);rewrite /partitions_aux !LgV//. move=> eql;rewrite /Vfs/inverse_fun/compose; aw. set_extens x. move /dirim_P => [y yW /compg_pP [z pa /igraph_pP pb]]. have : inc z (Vfs g (Vg f i)) by apply /dirim_P; ex_tac. rewrite eql; move /dirim_P => [x' x'Vf Jg2]. by rewrite (injective_pr3 inh pb Jg2). move=> xW. have xsh: inc x (source h) by rewrite sh; apply: (Ht _ idp). have : (inc (Vf h x) (Vfs h (Vg f i))). apply /dirim_P; ex_tac; Wtac. rewrite -eql; move /dirim_P => [x' x'Vf Jg]. apply /dirim_P; ex_tac; apply /compg_pP; ex_tac; apply /igraph_pP;Wtac. move=> aux; apply: Lg_exten. move=> i xdp; move: (aux _ xdp) => aux'. set_extens x. move /(dirim_P) => [y yVf Jg]. have xt:inc x (target h) by rewrite th -tg ;apply: (p2graph_target fg Jg). move: (p1graph_source fg Jg) =>ys. move: (sjh _ xt)=> [z zs Wz]. have p2: inc (J z x) (graph h) by rewrite Wz;apply: Vf_pr3 =>//. apply /dirim_P; ex_tac; rewrite -(aux _ xdp). apply /dirim_P; exists y => //; rewrite corresp_g; apply /compg_pP. by exists x=> //; rewrite /inverse_fun; aw; apply /igraph_pP. rewrite -{1} aux'/Vfs/compose /inverse_fun. rewrite !corresp_g; move /(dirim_P)=> [u] /(dirim_P) [v Jg]. move /compg_pP =>[w pa /igraph_pP pb] pc. apply /dirim_P; ex_tac; rewrite - (fgraph_pr _ pb pc); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)