proposition: Lemma Exercise6_31_g_unused: exists2 x, inc x inf_subsets & inc (A -s x) inf_subsets.
proof: Proof. move/infinite_setP: Ainf => icA. move: (disjointU2_pr3 A A C0_ne_C1); move: (csum_inf1 icA); set c := cardinal A => h. rewrite - csum2cr - csum2cl h double_cardinal. move /esym / equipotent_ex_pr1; set f := (equipotent_ex _ _). move =>[bf sf tf]. have ff: function f by fct_tac. set X := Vfs f (A *s1 C1). have sXA: sub X A by rewrite - tf; apply:(fun_image_Starget1 ff). have s1: sub (A *s1 C1) (source f) by rewrite sf => t; apply: setU2_1. move: (cardinal_image s1 (proj1 bf)); rewrite -/X cardinal_indexed => cc. have ra: inc X inf_subsets. by apply: Zo_i; [ by apply/setP_P | apply/infinite_setP; rewrite cc]. set Y := Vfs f (A *s1 C0). have sYA: sub Y A by rewrite - tf; apply:(fun_image_Starget1 ff). have s2: sub (A *s1 C0) (source f) by rewrite sf => t; apply: setU2_2. move: (cardinal_image s2 (proj1 bf)); rewrite -/Y cardinal_indexed => ccc. have rb: inc Y inf_subsets. by apply: Zo_i; [ by apply/setP_P | apply/infinite_setP; rewrite ccc]. have XY: Y = A -s X. set_extens t. move/(Vf_image_P ff s2) =>[u ua ->]; apply/setC_P; split; first Wtac. move/(Vf_image_P ff s1) =>[v va sv]. move: (proj2 (proj1 bf) u v (s2 _ ua) (s1 _ va) sv) => sv1. case: C0_ne_C1. move/indexed_P: ua => /proj33 <-. by move/indexed_P: va => /proj33 <-; rewrite sv1. move => /setC_P [sa]. rewrite - tf in sa; move: (proj2(proj2 bf) _ sa); rewrite sf. move => [i /setU2_P ii ->] sb; case:ii => ts. by case: sb; apply /(Vf_image_P ff s1); exists i. by apply /(Vf_image_P ff s2); exists i. by exists X => //; rewrite - XY. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)