proposition: Lemma Exercise6_31_C x y: inc x F -> (inc y (f x) <-> exists a b, [/\ sub a A, finite_set a, sub b x, infinite_set b & y = a \cup b]).
proof: Proof. move => xF; apply: (iff_trans (@Exercise6_31_B x y xF)); split. move => [qa qb]. have e1: y = (y -s x) \cup (y \cap x). set_extens t; last by case/setU2_P; [case/setC_P | move/setI2_1]. move => ty; case: (inc_or_not t x) => tx. by apply/setU2_P; right; apply/setI2_P. by apply/setU2_P; left; apply/setC_P. move: (Zo_S qa) => /Zo_P [/setP_P yA yi]. case: (finite_or_infinite_set(y \cap x)) => fi. by move: (finite_union2 qb fi); rewrite - e1 => /finite_not_infinite_set. have dA: sub (y -s x) A by move => t /setC_P [/ yA]. by exists (y -s x), (y \cap x); split => //; apply: subsetI2r. move => [a [b [aA fA bx ib yv]]]. move/Zo_P: (xF) => [/Zo_P [/setP_P xA xi] xc]. have yA :sub y A. by move => t;rewrite yv; case/setU2_P; [ apply: aA | move/bx /xA]. have syb: sub b y by rewrite yv; apply:subsetU2r. have iy:= (sub_infinite_set syb ib). have cy: countable_set y. apply/countableP. move: (countable_sub bx xc) => /countableP cb. move/infinite_setP: ib => cbi. move: (csum2_pr6 a b). rewrite - csum2cl - csum2cr (csum_fin_infin fA cbi) - yv => ll. apply: (cleT ll cb). have yF: inc y F by apply: Zo_i cy; apply: Zo_i iy; apply/setP_P. split => //; apply:sub_finite_set fA. by move => t; rewrite yv; move=> /setC_P [/setU2_P]; case => //; move/bx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)