proposition: Lemma nbsurj_rec n p: natp n -> natp p -> nbsurj (csucc n)(csucc p) = (csucc p) *c ( nbsurj n p +c nbsurj n (csucc p)).
proof: Proof. move => nN pN; rewrite {1} /nbsurj csumC. move: (NS_succ pN) => spN. set I := (Nint (csucc n)); set J:= (Nint (csucc p)). set I' := Nint n. set E := (surjections I J). pose phi := Lf (fun f => Vf f n) E J. have sphi: E = source phi by rewrite /phi; aw. have pa: csucc p = cardinal (target phi). by rewrite /phi; aw; rewrite (card_Nint spN). rewrite {1} pa sphi; clear pa. have lfa: lf_axiom (Vf ^~n) E J. move => f /Zo_P [] /functionsP [pa pb pc] _. by Wtac; rewrite pb; apply:Nint_si. have fphi: function phi by apply: lf_function. apply:(shepherd_principle fphi). rewrite {1} /phi; aw; move => x xJ. set F := Vfi1 phi x. have fp: forall f, inc f F <-> inc f (surjections I J) /\ x = Vf f n. move => f; split. move /(iim_fun_set1_P _ fphi) => []; rewrite - sphi => fe. rewrite{1}/phi LfV//. move => [pa pb]; apply /(iim_fun_set1_P _ fphi). split => //;[ ue | rewrite /phi LfV//]. pose sfx f := exists2 y, inc y I' & Vf f y = x. have ii': sub I' I by apply: Nint_M. set A1 := Zo F sfx. have <-: cardinal A1 = nbsurj n (csucc p). apply /card_eqP. exists (Lf (restriction^~ I' ) A1 (surjections I' J)); saw. apply /lf_bijective. move => f /Zo_P [] /fp [] /Zo_P [] /functionsP [ff sf tf] sjf fn sff. have si: sub I' (source f) by rewrite sf. move: (restriction_prop ff si); rewrite tf => fp'. apply /Zo_P; split; first by apply /functionsP. move: fp' => [sa sb sc]; split; first by exact. rewrite sc sb - tf=> y ytf; move: (proj2 sjf _ ytf) => [a asf va]. move: asf; rewrite sf; move /(NintsP nN) => lean. case: (equal_or_not a n) => lan. move: sff => [b ba bb]; rewrite va lan - fn - bb; ex_tac. rewrite restriction_V //. have aI: inc a I' by apply /(NintP nN). by exists a => //; rewrite restriction_V. move => f g /Zo_P [] /fp [] /Zo_P [] /functionsP [ff sf tf] sjf fn sff. move => /Zo_P [] /fp [] /Zo_P [] /functionsP [fg sg tg] sjg gn sfg sr. apply: function_exten => //; (try ue); move => i isf /=. move: isf; rewrite sf; move /(NintsP nN) => lein. case: (equal_or_not i n) => lin; first by rewrite lin - fn gn. have iI: inc i I' by apply /(NintP nN); split. have si: sub I' (source f) by rewrite sf. have sj: sub I' (source g) by rewrite sg - sf. move: (f_equal (Vf^~ i) sr); rewrite restriction_V // restriction_V //. move => y /Zo_P [] /functionsP [fy sy ty] sjy. move: (Nint_pr4 nN); rewrite -/I -/I' - sy; move => [ci pa]. move:(extension_fs x fy pa sjy) => sjf. have pb: sub I' (source (extension y n x)). by rewrite /extension sy; aww. move:(proj1 sjf) => fjf. have si: source (extension y n x) = I by rewrite /extension; aw. have ti: target (extension y n x) = J. rewrite /extension ty; aw; rewrite setU1_eq //. have fx: Vf (extension y n x) n = x by rewrite extension_Vf_out. have re : (restriction (extension y n x) I') = y. move: (restriction_prop fjf pb) => [pc pd pe]. apply : function_exten => //; rewrite ? pd ?pe ? ti//. move => i ii /=;rewrite restriction_V //. by rewrite extension_Vf_in // sy. have aux: sfx (extension y n x). rewrite -ty in xJ; move: (proj2 sjy _ xJ) => [s sa sb]. exists s; [ ue | rewrite extension_Vf_in //]. exists (extension y n x);last by ue. by apply:Zo_i=> //;apply /fp; split => //; apply:Zo_i=> //; apply /functionsP. have sa1: sub A1 F by apply: Zo_S. rewrite (cardinal_setC2 sa1) csum2cl - csum2cr; congr (_ +c _). have pa: n = cardinal I' by rewrite (card_Nint nN). have fs1: finite_set I' by apply:finite_Nint. have pb: p = cardinal (J -s1 x). by rewrite - (cpred_pr5 xJ) (card_Nint spN) cpred_pr2. have fs2: finite_set (J -s1 x) by apply/NatP;rewrite -pb. rewrite pa pb - (nbsurj_pr fs1 fs2). apply /card_eqP. have pc: forall f, inc f (F -s A1) -> restriction2_axioms f I' (J -s1 x). move => f /setC_P [fF fp1]. move: (fF) => /fp [] /Zo_P[] /functionsP [ff sf tf] sjf fn. have aux: sub I' (source f) by ue. red; rewrite sf tf; split => //; try apply: sub_setC. move => i /(Vf_image_P ff aux) [u ui ->]; apply /setC1_P; split. rewrite -tf; Wtac. by dneg fa1; apply /Zo_P;split => //; exists u. exists (Lf (fun z => restriction2 z I' (J -s1 x)) (F -s A1) (surjections I' (J -s1 x))); saw. apply /lf_bijective. move => f fa /=; move: (pc _ fa) => a1. move: (restriction2_prop a1) => a2. move: fa => /Zo_P [] /fp [] /Zo_P [] /functionsP [ff sf tf] sjf fn sff. apply /Zo_P;split; first by apply /functionsP. move: a2 => [a3 a4 a5]; split; first by exact. rewrite a4 a5 - {1} tf=> y /setC1_P [ytf xx]. move: (proj2 sjf _ ytf) => [a asf va]. move: asf; rewrite sf; move /(NintsP nN) => lean. case: (equal_or_not a n) => lan; first by case: xx; rewrite fn va lan. have aI: inc a I' by apply /(NintP nN); split. by exists a => //; rewrite restriction2_V. move => f g fa fb sr. move: (pc _ fa) (pc _ fb) => a1 a2. move: fa => /setC_P [] /fp [] /Zo_P [] /functionsP [ff sf tf] _ fv _. move: fb => /setC_P [] /fp [] /Zo_P [] /functionsP [fg sg tg] _ gv _. apply: function_exten => //; (try ue); move => i isf /=. move: isf; rewrite sf; move /(NintsP nN) => lein. case: (equal_or_not i n) => lin; first by rewrite lin - fv gv. have iI: inc i I' by apply /(NintP nN); split. move: (f_equal (Vf^~ i) sr); rewrite restriction2_V // restriction2_V //. move => y /Zo_P [] /functionsP [fy sy ty] sjy. move: (Nint_pr4 nN); rewrite -/I -/I' - sy; move => [ci pd]. move:(extension_fs x fy pd sjy) => sjf. have pe: sub I' (source (extension y n x)). by rewrite /extension sy; aww. move:(proj1 sjf) => fjf. have si: source (extension y n x) = I by rewrite /extension; aw. have ti: target (extension y n x) = J. by rewrite /extension ty; aw; apply:setC1_K. have fx: Vf (extension y n x) n = x by rewrite extension_Vf_out. move: (extension_restr x fy pd); rewrite ty => pf. exists (extension y n x) => //; apply/setC_P; split. by apply /fp; split => //; apply /Zo_P; split => //; apply /functionsP. move /Zo_P => [sa [z]]; rewrite - sy => sb;rewrite extension_Vf_in // => pg. by move: (Vf_target fy sb); rewrite pg ty => /setC1_P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)