proposition: Lemma CantorBernstein_v4 E F f g (gi := fun y => union (Vfi1 g y)) (fi := fun y=> union (Vfi1 f y)) (alpha := J C0 C2) (pE:= fun x => Yo (inc x (Imf g) )(J (gi x) C1) alpha) (pF := fun y => Yo (inc y (Imf f)) (J (fi y) C0) alpha) (p := fun x => Yo (Q x = C2) x (Yo (Q x = C0) (pE (P x)) (pF (P x)))) (pn := induction_term (fun _ v => p v)) (fv := fun x n => [/\ natp n, pn x n = alpha & forall m, m <c n -> pn x m <> alpha]) (to := fun x => exists2 n, oddp n & fv x n) (h1 := fun x => Yo (to x) (Vf f (P x)) (P (p x))) (h := fun x => h1 (J x C0)): injection_prop f E F -> injection_prop g F E -> bijection_prop (Lf h E F) E F.
proof: Proof. move => [[ff finj] sf tf] [[fg ginj] sg tg]. pose E0 := indexed E C0. pose F1 := indexed E C1. move:C2_ne_C01 => [qa qb]. have aE0: ~inc alpha E0 by rewrite /alpha; move/setX_P => /proj33/set1_P; aw. have aF1: ~inc alpha F1 by rewrite /alpha; move/setX_P => /proj33/set1_P; aw. have fip x: inc x E -> fi (Vf f x) = x. move => xE; rewrite /fi. suff: (Vfi1 f (Vf f x)) = singleton x by move ->; rewrite setU_1. apply: set1_pr; first by apply:(iim_fun_set1_i ff) => //; ue. move => t ta; move/ (iim_fun_set1_P (Vf f x) ff): ta => [tsf eq1]. apply: finj => //; ue. have gip x: inc x F -> gi (Vf g x) = x. move => xE; rewrite /gi. suff: (Vfi1 g (Vf g x)) = singleton x by move ->; rewrite setU_1. apply: set1_pr; first by apply:(iim_fun_set1_i fg) => //; ue. move => t ta; move/ (iim_fun_set1_P (Vf g x) fg): ta => [tsf eq1]. apply: ginj => //; ue. have pE1 y: inc y F -> (pE (Vf g y)) = J y C1. rewrite /pE => yF; Ytac w; [ by rewrite gip | case:w; apply: (Imf_i fg);ue]. have pF1 x: inc x E -> (pF (Vf f x)) = J x C0. rewrite /pF => yF; Ytac w; [ by rewrite fip | case:w; apply: (Imf_i ff);ue]. have pE2 y: inc y F -> (p (J (Vf g y) C0)) = J y C1. by rewrite/p;aw; move => /pE1 ->; Ytac0; Ytac0. have pF2 x: inc x E -> (p (J (Vf f x) C1)) = J x C0. by rewrite/p;aw; move => /pF1 ->; Ytac0; Ytac0. have pa: p alpha = alpha by rewrite /p/alpha ;aw; Ytac0; Ytac0. have pna x: pn x \0c = x by rewrite /pn induction_term0. have pnb x n: natp n -> pn x (csucc n) = p (pn x n). by apply: induction_terms. have toq x: inc x E -> (to (J x C0) <-> to (J (Vf g (Vf f x)) C0)). move => xE. have fxF: inc (Vf f x) F by Wtac. have gfxE: inc (Vf g (Vf f x)) E by Wtac. move: (pF2 _ xE)(pE2 _ fxF); set z := (Vf g (Vf f x)) => py pz. have pr: forall n, natp n -> pn (J z C0) (csucc (csucc n)) = pn (J x C0) n. apply: Nat_induction. by rewrite (pnb _ _ (NS_succ NS0)) (pnb _ _ NS0) pna pna pz py. move => n nN hrec; rewrite (pnb _ _ nN) - hrec pnb; fprops. have p0: pn (J z C0) \0c <> alpha. by rewrite pna => /pr2_def; apply: nesym. have p1: pn (J z C0) \1c <> alpha. by rewrite - succ_zero (pnb _ _ NS0) pna pz => /pr2_def; apply: nesym. have qc m: natp m -> pn (J z C0) m = alpha -> exists2 q, natp q & m = csucc (csucc q). move => mN pp. case: (equal_or_not m \0c) => m0; first by case: p0; rewrite - m0. move: (cpred_pr mN m0)=> [sa sb]. case: (equal_or_not (cpred m) \0c) => m1. by case: p1; rewrite - pp sb m1 succ_zero. move: (cpred_pr sa m1) =>[sc sd]; exists (cpred (cpred m)) => //; ue. split; move => [n on [nN hb hc]]. exists (csucc (csucc n)). by apply: succ_of_even; apply: succ_of_odd. split; [ fprops | by rewrite pr | move => m mls pb]. move: (qc m (NS_lt_nat mls (NS_succ (NS_succ nN))) pb) => [q qN qv]. move: mls; rewrite qv; move/(cltSSP (CS_succ q)(CS_succ n)). move/(cltSSP (CS_nat qN)(CS_nat nN)) => lqn. by case: (hc _ lqn); rewrite - (pr _ qN) - qv. move: (qc n nN hb) =>[q qN qv]; exists q. split => // eqv; case: on => _; case; rewrite qv. by apply: succ_of_odd; apply: succ_of_even. split; [ done | by rewrite -(pr _ qN) - qv | move => m lmn]. rewrite -(pr _ (NS_lt_nat lmn qN)). by apply: hc; rewrite qv; apply: cltSS ; apply: cltSS. have hp1 x: to (J x C0) -> h x = Vf f x. by move => tox;rewrite /h/h1; Ytac0; aw. have hp2 x: inc x E -> to (J x C0) -> inc (h x) F. move => xe tox; rewrite hp1 //;Wtac. have hp3 x: ~ to (J x C0) -> h x = P (pE x). by move => rox; rewrite /h/h1/p; Ytac0; aw; Ytac0; Ytac0. have hp7 x : inc x E -> ~ inc x (Imf g) -> to (J x C0). move => xE xi; exists \1c; [ by apply: odd_one | split ]. - apply: NS1. - rewrite - (succ_zero) (pnb _ _ NS0) pna. by rewrite /p/pE; aw; Ytac0; Ytac0; Ytac0. - by move => m /clt1 ->; rewrite pna => /pr2_def; apply: nesym. have hp4 x: inc x E -> ~ to (J x C0) -> [/\ inc x (Imf g), h x = (gi x), inc (h x) F & Vf g (h x) = x]. move => xE tox. case: (inc_or_not x (Imf g)) => xi; last by case: tox; apply: hp7. rewrite (hp3 _ tox). have-> : P (pE x) = gi x by rewrite /pE; Ytac0; aw. move/(Imf_P fg): (xi) =>[u usg uv]; rewrite sg in usg. by move: (gip _ usg); rewrite - uv => ->. have hp5 x: inc x E -> inc (h x) F. move => xE; case: (p_or_not_p (to (J x C0))); first by apply: hp2. by move => tox; case: (hp4 x xE tox). have hp6 y: inc y F -> ~ to (J (Vf g y) C0) -> y = h (Vf g y). move => yF hb; have xE: inc (Vf g y) E by Wtac. by move: (hp4 _ xE hb) =>[hc hd he hf]; rewrite hd (gip _ yF). have sjf y: inc y F -> exists2 x, inc x E & y = h x. move => yF. case: (inc_or_not y (Imf f)) => yi; last first. set x := (Vf g y). have xE: inc x E by rewrite/x; Wtac. ex_tac. case: (p_or_not_p (to (J x C0))); last by move => /(hp6 y yF). move =>[m om [ma mb mc]]. have eq3: p (J x C0) = J y C1 by exact: (pE2 _ yF). have eq4: pn (J x C0) \1c = J y C1. by rewrite - succ_zero (pnb _ _ NS0) pna eq3. have eq5: pn (J x C0) \2c = alpha. by rewrite - succ_one (pnb _ _ NS1) eq4 /p/pF; aw;Ytac0; Ytac0; Ytac0. case: (equal_or_not m \0c) => mz. case: om => _ []; rewrite mz; apply: even_zero. case: (equal_or_not m \1c) => mo. by move: mb; rewrite mo eq4 => /pr2_def hw; case: qb. move: (cge2 (CS_nat ma) mz mo); case/cle_eqVlt => mt. case: om => [_ []]; rewrite - mt; apply: even_two. by case: (mc _ mt). move/(Imf_P ff): (yi) =>[x xE xv]; rewrite sf in xE. case: (p_or_not_p (to (J x C0))) => tox. by exists x => //; rewrite xv hp1. set z := (Vf g y). have zE: inc z E by rewrite/z; Wtac. case: (p_or_not_p (to (J z C0))) => toz; last first. ex_tac; exact:(hp6 y yF toz). by case: tox; apply/ (toq _ xE); rewrite - xv. saw; apply: lf_bijective => // u v uE vE sh. case: (p_or_not_p (to (J u C0)))=> tou; case:(p_or_not_p (to (J v C0))) => tov. - by move: sh; rewrite (hp1 _ tou) (hp1 _ tov); apply: finj; ue. - move: sh; rewrite (hp1 _ tou) => hv. move: (hp4 v vE tov) =>[ra rb rc rd]. by case: tov; rewrite - rd - hv; apply/ (toq u uE). - move: sh; rewrite (hp1 _ tov) => hv. move: (hp4 u uE tou) =>[ra rb rc rd]. by case: tou; rewrite - rd hv; apply/ (toq v vE). - by rewrite -(proj44 (hp4 v vE tov)) - (proj44 (hp4 u uE tou)) sh. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)