proposition: Lemma nbsurj_inv n p: natp n -> natp p -> p ^c n = csumb (Nintc p) (fun k => (binom p k) *c (nbsurj n k)).
proof: Proof. move => nN pN. set I := (Nint n); set J:= (Nint p). have ci: n = cardinal I by rewrite (card_Nint nN). have cj: p = cardinal J by rewrite (card_Nint pN). set K := (Nintc p). have ->: p ^c n = cardinal (functions I J). by rewrite ci cj; apply:cpow_pr; aw. have pa: forall x, inc x (functions I J) -> sub (Imf x) J. by move => x /functionsP [p1 p2 <-]; apply:Imf_Starget. have pb: forall x, inc x (functions I J) -> inc (cardinal (Imf x)) K. move => x h; move: (sub_smaller (pa _ h)). by rewrite - cj; move /(NintcP pN). rewrite (card_partition_induced pb); apply: csumb_exten => k. move/(NintcP pN) => kp. move: (NS_le_nat kp pN) => kN. rewrite - (card_p_subsets pN kN (sym_eq cj)). set E1 := Zo _ _; set K1 := subsets_with_p_elements _ _. have pc: forall c, inc c E1 -> inc (Imf c) K1. by move => c /Zo_P [pc pd]; apply /Zo_P;split => //; apply /setP_P; apply: pa. pose phi := Lf Imf E1 K1. have sphi: E1 = source phi by rewrite /phi; aw. have tphi: K1 = target phi by rewrite /phi; aw. have fphi: function phi by apply: lf_function. rewrite sphi tphi; apply: (shepherd_principle fphi). move => tf; rewrite - tphi; move /Zo_P => [] /setP_P tfj ctf. set K2:= Zo (functions I J) (fun f => Imf f = tf). have ->: Vfi1 phi tf = K2. set_extens t. move /(iim_fun_set1_P _ fphi) => []; rewrite - sphi /phi => t1. rewrite LfV//. move /Zo_P: t1 => [t1 t2] t3; apply /Zo_P;split => //. move => /Zo_P [t1 t2]; apply /(iim_fun_set1_P _ fphi); rewrite - sphi. have te1: inc t E1 by apply /Zo_P; rewrite t2. by rewrite /phi LfV//. rewrite ci - ctf. rewrite - nbsurj_pr; try apply/NatP; [ | by rewrite - ci | by rewrite ctf]. apply /card_eqP. exists (Lf restriction_to_image K2 (surjections I tf)); saw. apply: lf_bijective. move => c /Zo_P [] /functionsP [qa qb qc] qd; apply /Zo_P. move: (restriction_to_image_fs qa) => qe;split => //; apply /functionsP. move: (proj1 qe) => f. by hnf;rewrite{2 3} /restriction_to_image /restriction2; aw; split. move => u v /Zo_P [] /functionsP [qa qb qc] qd. move => /Zo_P [] /functionsP [ra rb rc] rd sr. apply: function_exten => //; rewrite ? rb ? rc // => x xI. move: (f_equal (Vf ^~x) sr). move: (restriction_to_image_axioms qa) => h; rewrite restriction2_V //. move: (restriction_to_image_axioms ra) => h'; rewrite restriction2_V //. by rewrite rb - qb. move => y /Zo_P [] /functionsP [qa qb qc] qd. set f := Lf (Vf y) I J. have fa: forall z, inc z I -> inc (Vf y z) J. rewrite -qb; move => z zi; apply: tfj; rewrite -qc; Wtac. have fb: function f by apply: lf_function. have sfi: source f = I by rewrite /f;aw. have fc: Imf f = tf. set_extens t. move /(Imf_P fb); rewrite sfi; move => [u u1 ->]; rewrite /f LfV//. Wtac. rewrite -qc => tt; move: (proj2 qd _ tt); rewrite qb; move => [u u1 u2]. by apply /(Imf_P fb); rewrite sfi;ex_tac; rewrite /f LfV. have fd:inc f K2 by apply/ Zo_P;split => //;apply/functionsP;rewrite /f;red;aw. have ra:= (proj1 (restriction_to_image_fs fb)). have rb:= (restriction_to_image_axioms fb). have sr:source (restriction_to_image f) = source y by rewrite corresp_s sfi. ex_tac; apply: function_exten => //. by rewrite corresp_t fc. by rewrite qb;move => t ts; rewrite restriction2_V // -? sfi // /f? LfV//; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)