proposition: Lemma Exercise6_12g n: natp n -> factorial n = cardinal (fun_image (permutations (Nint1c n)) (fun s => oprodf (fun i => (omega0 +o Vf s (csucc i))) n)).
proof: Proof. move => nN. move: (card_Nint1c nN); set F := (Nint1c n) => cf. have fsf: finite_set F by red; rewrite cf; apply /NatP. set f := (fun s : Set => _). rewrite - cf - (card_permutations fsf). apply /card_eqP. set E := permutations F; exists (Lf f E (fun_image E f)); saw. have H: forall s, inc s E -> Ex6_12_ax (Vf s) n. move => s /Zo_P [] /functionsP [fs ss ts] _ i ii. have: inc (Vf s i) F by rewrite - ts; Wtac; rewrite ss. move /(Nint1cP nN) => [sa sb]; exact:(posnat_prop (NS_le_nat sb nN) sa). apply: lf_bijective. + move => t te; apply /funI_P; ex_tac. + move => u v ue ve. move: (H _ ue) (H _ ve) => ax1 ax2. rewrite /f - (Exercise6_12f nN ax1) - (Exercise6_12f nN ax2) => eq. move: (Exercise6_12c nN ax1 ax2 eq) => h. move: ue ve => /Zo_S /functionsP [fs ss ts] /Zo_S /functionsP [fs' ss' ts'] . apply: function_exten; [exact | exact | by rewrite ss' | by rewrite ts'|]. by move => i; rewrite ss; apply: h. + by move => t /funI_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)