proposition: Lemma nds_card_perm_inv X n g: natp n -> nds_ax X n -> inc g (permutations n) -> nds_card X n = nds_card (fun z => X (Vf g z)) n.
proof: Proof. move => nN ax /Zo_P [] /functionsP [fg sg tg] bg. rewrite /nds_card /nds_sums; apply: f_equal. set E := permutations n. set_extens t; move /funI_P => [z ze ->]; apply /funI_P. move: (inverse_bij_fb bg) => ibg. move: ze =>/permutationsP [bz sz tz]; move:(proj1 (proj1 bz)) => fz. have fa: (inverse_fun g) \coP z by hnf;aw;split => //; [fct_tac | ue]. have fb: function ((inverse_fun g) \co z) by fct_tac. exists ((inverse_fun g) \co z). apply: Zo_i; [ apply /functionsP;red;saw | by apply compose_fb ]. apply:(osumf_exten nN) => i lin. have iz: inc i (source z) by rewrite sz; apply /(NltP nN i). have cp: inverse_fun g \coP z by split; [ fct_tac | exact | aw; ue]. have fzy: inc (Vf z i) (target g) by rewrite tg - tz; Wtac. by rewrite (compfV cp iz) (inverse_V bg fzy). move: ze => /permutationsP [bz sz tz]; move:(proj1 (proj1 bz)) => fz. have fa: g \coP z by red;saw; ue. have fb: function (g \co z) by fct_tac. exists (g \co z). apply: Zo_i; [ apply /functionsP;red;saw | by apply compose_fb ]. apply:(osumf_exten nN) => i lin. by rewrite compfV // sz; apply/(NltP nN i). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)