proposition: Lemma Exercise6_6a: exists G, [/\ sub G E, G =c E & (E -s G) =c F].
proof: Proof. move: Einf => /infinite_setP ise1. move:(csum_inf leFE ise1); aw. have pc:= (disjointU2_pr3 E F C1_ne_C0). rewrite csum2cl csum2cr -(card_card (CS_sum2 E F)) pc. set E1:= E *s1 C0; set F1:= F *s1 C1. move=> /card_eqP [f [bf sf tf]]. move: (bf) => [injf sjf]. have sc1: sub E1 (source f) by rewrite sf; apply: subsetU2l. have sc2: sub F1 (source f) by rewrite sf; apply: subsetU2r. have ff: function f by fct_tac. have sc3: sub (Vfs f E1) (target f) by apply: fun_image_Starget1. exists (Vfs f E1); split => //; first by rewrite -tf. by rewrite (cardinal_image sc1 injf) /E1; aw. move: (inj_image_C injf (refl_equal (source f)) sc1). have ->: (source f) -s E1 = F1. rewrite sf setCU2_l setC_v set0_U2; set_extens t;first by move => /setC_P []. move => ta; apply /setC_P;split => // /indexed_P [_ _ qa]. move /indexed_P: ta => [_ _]; rewrite qa; fprops. rewrite -/(Imf f) (surjective_pr0 sjf) tf => <-. by rewrite (cardinal_image sc2 injf)/F1; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)