proposition: Lemma Exercise6_31_k z (X0 := rep z) (Xn := Ex6_31_Xnz z) : inc z Z -> [/\ Xn \0c = X0, forall n, natp n -> inc (Xn n) F, forall n, natp n -> sub (Xn (csucc n)) (Xn n), forall n, natp n -> infinite_set ((Xn n) -s (Xn (csucc n))) & intersectionf Nat Xn = emptyset].
proof: Proof. move => zZ. set g := (equipotent_ex Nat X0). move: (Exercise6_31_A zZ); rewrite -/X0; move =>[X0F le0]. move/Zo_P: X0F => [/Zo_P [/setP_P xc xa] xb]. have [bg sg tg]: bijection_prop g Nat X0. case: (countable_finite_or_N xb); first by move /finite_not_infinite_set. by rewrite aleph0_pr1; move/esym /card_eqP/equipotent_ex_pr. move: (equipotent_ex_pr equipotent_N2_N). set h := equipotent_ex _ _; move => [bh sh th]. have ra n: sub (Xn n) X0 by apply: Zo_S. have fg: function g by fct_tac. have fh: function h by fct_tac. have comp_inj i j i1 j1: natp i -> natp j -> natp i1 -> natp j1 -> Vf g (Vf h (J i j)) = Vf g (Vf h (J i1 j1)) -> i = i1 /\ j = j1. move => iN jN i1N j1N. have sa1: inc (J i j) (source h) by rewrite sh; apply: setXp_i. have sa: inc (Vf h (J i j)) (source g) by rewrite sg - th; Wtac. have sb1: inc (J i1 j1) (source h) by rewrite sh; apply: setXp_i. have sb: inc (Vf h (J i1 j1)) (source g) by rewrite sg - th; Wtac. move/ (proj2 (proj1 bg) _ _ sa sb). by move/ (proj2 (proj1 bh) _ _ sa1 sb1) => /pr12_def. have rb: Xn \0c = X0. set_extens t; first by move/Zo_S. move => tx0; apply: Zo_i => //. rewrite - tg in tx0. move: (proj2 (proj2 bg) _ tx0); rewrite sg. move => [x xN ->]. rewrite -th in xN; move: (proj2 (proj2 bh) _ xN); rewrite sh. move => [ij /setX_P [qa qb qc] ->]. exists (P ij), (Q ij); split => //; [ by apply: cle0n | by rewrite qa]. have re: intersectionf Nat Xn = emptyset. have nen: nonempty Nat by exists \0c; apply: NS0. apply/set0_P => t /(setIf_P _ nen) hyp. move: (hyp _ NS0) => /Zo_hi [i [j [iN jN _ tv]]]. move: (hyp _ (NS_succ iN)) => /Zo_hi [i1 [j1 [i1N j1N la]]]. rewrite tv. move/(comp_inj _ _ _ _ iN jN i1N j1N) => /proj1 ii. by case: (proj2 (clt_leT (cltS iN) la)). have rf n : natp n -> sub (Xn (csucc n)) (Xn n). move => nN t /Zo_P [tX [i [j [iN jN lin ee]]]]; apply:Zo_i => //. by rewrite ee; exists i, j; split => //; move: (cleT (cleS nN) lin). have rd1 n: natp n -> Xn n -s Xn (csucc n) = fun_image Nat (fun z => (Vf g (Vf h (J n z)))). move => nN;set_extens t. move => /setC_P [/Zo_P [ha [i [j [iN jN kin tv]]] hc]]. case: (equal_or_not n i) => ein. by apply/funI_P; exists j => //; rewrite ein. case: hc; apply:Zo_i => //; exists i, j; split => //. by apply/(cleSltP nN). move =>/funI_P[j jN ->]; apply/setC_P; split. apply: Zo_i. rewrite -/X0 - tg; Wtac; rewrite sg - th; Wtac. by rewrite sh; apply: setXp_i. exists n, j; split => //; apply: (cleR (CS_nat nN)). move=> /Zo_hi [i1 [j1 [i1N j1N le1]]]. move/(comp_inj _ _ _ _ nN jN i1N j1N) => /proj1 ee. by case: (cleNgt le1); rewrite - ee; apply:cltS. have rd n: natp n -> infinite_set (Xn n -s Xn (csucc n)). move => nN; rewrite (rd1 _ nN); apply/infinite_setP. rewrite cardinal_fun_image; first by apply/infinite_setP /infinite_Nat. by move => i1 i2 i1N i2N; move/(comp_inj _ _ _ _ nN i1N nN i2N); case. split => //. move => n nN. have qa: infinite_set (Xn n). have /sub_smaller la: sub (Xn n -s Xn (csucc n)) (Xn n). by move => t/setC_P; case. move/infinite_setP: (rd _ nN) => sa. by move: (cle_inf_inf sa la); move/infinite_setP. move: (countable_sub (ra n) xb) => cs. apply: Zo_i => //. apply: Zo_i => //; apply/setP_P; apply:(sub_trans (ra n) xc). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)