proposition: Lemma nbsurj_pr E F: finite_set E -> finite_set F -> cardinal (surjections E F) = nbsurj (cardinal E) (cardinal F).
proof: Proof. move => /NatP nN /NatP mN. apply/card_eqP. set n := (cardinal E); set m := (cardinal F). set s:= (surjections E F);set t := surjections _ _. move/card_eqP:(card_Nint nN) => [g [fg sg tg]]. move/card_eqP:(card_Nint mN) => [h [fh sh th]]. move: (inverse_bij_fb fh) => bih. set j := (fun f => (inverse_fun h) \co f \co g). have pc: forall f, inc f s -> (inverse_fun h \coP f)/\ (inverse_fun h \co f) \coP g. move => f /Zo_P [] /functionsP [ff sf tf] sjf. have s1: inverse_fun h \coP f by split => //; aw; try fct_tac; ue. split => //; split => //; aw; try ue; try fct_tac. exists (Lf (fun f => (inverse_fun h) \co f \co g) s t). saw;apply: lf_bijective. move => f fp; move: (pc _ fp)=> [s1 s2]; apply/ Zo_P;split => //. apply /functionsP;red;saw; fct_tac. move/ Zo_hi: fp => sjf. move: (compose_fs sjf (proj2 bih) s1) => s3; apply:compose_fs => //. exact (proj2 fg). move => u v us vs; move: (pc _ us) (pc _ vs)=> [s1 s2][s3 s4] s5. move: (compf_regl fg s2 s4 s5) => s6. by move: (compf_regr bih s1 s3 s6). move => y /Zo_P []/functionsP [fy sy ty] sjy. set f := (h \co (y \co inverse_fun g)). move: (inverse_bij_fb fg) => big. have s1: (y \coP inverse_fun g) by saw; try fct_tac; ue. have s2: h \coP (y \co inverse_fun g) by saw; try ue; try fct_tac. have fs: inc f s. apply/ Zo_P; split. by rewrite /f;apply /functionsP;saw;try fct_tac. move: (compose_fs (proj2 big) sjy s1) => s3; apply:compose_fs => //. exact (proj2 fh). exists f => //; rewrite /f (compfA (composable_inv_f fh) s2). have pd: (source h) = target (y \co inverse_fun g) by aw; ue. rewrite (bij_left_inverse fh) pd (compf_id_l (proj32 s2)). rewrite - (compfA s1 (composable_inv_f fg)) (bij_left_inverse fg) sg - sy. by symmetry;apply (compf_id_r). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)