proposition: Lemma nds_card_shift n X: natp n -> nds_ax X n -> nds_card X n = nds_card (fun i => nds_shift (X i)) n.
proof: Proof. move => nN ax. rewrite /nds_card /nds_sums. set E := permutations n; set A := fun_image _ _;set B := fun_image _ _. apply /card_eqP; exists (Lf nds_shift A B). have aux f: inc f E -> ordinalp (nds_sc X n f) /\ nds_sc (fun i => nds_shift (X i)) n f = nds_shift(nds_sc X n f). move => /permutationsP[bf sf tf]; apply:(osum_shift nN). move => i /(NltP nN) tn; apply: ax;apply/(NltP nN); Wtac; fct_tac. saw;apply:lf_bijective. + move => z /funI_P [f fp ->]; apply /funI_P; exists f => //. by rewrite (proj2 (aux _ fp)). + move => u v /funI_P [a az ->] /funI_P [b bz ->]. move:(proj1 (aux _ az)) (proj1 (aux _ bz)) => sa sb. apply: (oprod2_simpl sa sb (oopow_pos OS2)). + move => z /funI_P [f fp ->]; exists(nds_sc X n f). apply /funI_P; exists f => //. by apply: (proj2 (aux _ fp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)