proposition: Lemma Exercise6_6b: (functions E F) =c (surjections E F).
proof: Proof. move: Exercise6_6a => [G [sGE /card_eqP[f [bf sf tf]] /card_eqP[g [bg sg tg]]]]. symmetry;apply: cleA; first by apply: sub_smaller; apply: Zo_S. pose C h x := Yo (inc x G) (Vf h (Vf f x)) (Vf g x). pose Cx h := Lf (C h) E F. move: bf bg => [[ff _] sjf] [[fg _] sjg]. set s1 := (functions E F);set s3 := (surjections E F). have pd: forall u, inc u s1 -> lf_axiom (C u) E F. move=> u /functionsP [fu su tu]. move=> t te; rewrite /C; Ytac tG; [ rewrite -tu | rewrite -tg] ;Wtac. rewrite su -tf; Wtac. rewrite sg; apply /setC_P;split => //. have pe: forall u, inc u s1 -> surjection (Cx u). move=> u us1; move: (pd _ us1) => ta. apply: lf_surjective => // y yF; rewrite -tg in yF. move: ((proj2 sjg) _ yF) => [z zsg ->]. move: zsg; rewrite sg => /setC_P [ze nzg]; ex_tac. by rewrite /C; Ytac0. have pf: lf_axiom Cx s1 s3. move=> u us1; move: (pe _ us1) => sC. apply: Zo_i =>//; apply /functionsP; rewrite /Cx; red;saw; fct_tac. have pa: s1 = source (Lf Cx s1 s3) by aw. have pb: s3 = target (Lf Cx s1 s3) by aw. rewrite pb {1} pa;apply: inj_source_smaller; apply: lf_injective => //. move=> u v us1 vs1; move: (pd _ us1) (pd _ vs1) => ta1 ta2. move: us1 vs1 => /functionsP [fu su tu] /functionsP [fv sv tv] sC. apply: function_exten => //; try ue. move=> x; rewrite su -tf => xtf. move: ((proj2 sjf) _ xtf) => [y ysf ->]. rewrite sf in ysf; move: (sGE _ ysf) => yE. move: (f_equal (Vf^~y) sC); rewrite /Cx !LfV//. by rewrite /C; Ytac0 ; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)