proposition: Lemma tarski_lemma1 M A: Saleph A -> M \times A \Eq dsum M A -> A <=s M \/ M <=s A.
proof: Proof. move => [_ [r [wor osr]]] /EqS [f [bf sf tf]]. have ff: function f by fct_tac. pose M1 := fun_image M (fun z => Vf f (J z C0)). pose A1 := fun_image A (fun z => Vf f (J z C1)). have qm t: inc t M -> inc (Vf f (J t C0)) M1. move => tm; apply/funI_P; ex_tac. have qa t: inc t A -> inc (Vf f (J t C1)) A1. move => tm; apply/funI_P; ex_tac. have ha: sub M1 (M \times A). by move => t /funI_P [z zM ->]; Wtac; rewrite sf; apply: candu2_pra. have hb: sub A1 (M \times A). by move => t /funI_P [z zM ->]; Wtac; rewrite sf; apply: candu2_prb. have hc: M \times A = M1 \cup A1. set_extens t; last by case/setU2_P; fprops. rewrite - tf => /(proj2(proj2 bf)) [x xsf ->]. move: xsf; rewrite sf => /candu2P [pp]; case. by move =>[sa sb]; apply:setU2_1; apply/funI_P; ex_tac; rewrite - sb pp. by move =>[sa sb]; apply:setU2_2; apply/funI_P; ex_tac; rewrite - sb pp. have hd: disjoint M1 A1. apply/set0_P => t /setI2_P [/funI_P [a al ->] /funI_P [b bM bb]]. have asf : inc (J a C0) (source f) by rewrite sf; apply: candu2_pra. have bsf : inc (J b C1) (source f) by rewrite sf; apply: candu2_prb. move: (pr2_def (proj2 (proj1 bf) _ _ asf bsf bb)); fprops. pose fM := Lf (fun z => Vf f (J z C0)) M M1. pose fA := Lf (fun z => Vf f (J z C1)) A A1. have bfM: bijection_prop fM M M1. rewrite /fM;saw; apply: lf_bijective. - done. - move => u v uM vM sfv. have usf : inc (J u C0) (source f) by rewrite sf; apply: candu2_pra. have vsf : inc (J v C0) (source f) by rewrite sf; apply: candu2_pra. exact: (pr1_def (proj2 (proj1 bf) _ _ usf vsf sfv)). - by move =>y /funI_P. have bfA: bijection_prop fA A A1. rewrite /fA;saw; apply: lf_bijective. - done. - move => u v uM vM sfv. have usf : inc (J u C1) (source f) by rewrite sf; apply: candu2_prb. have vsf : inc (J v C1) (source f) by rewrite sf; apply: candu2_prb. exact: (pr1_def (proj2 (proj1 bf) _ _ usf vsf sfv)). - by move =>y /funI_P. have he: M \Eq M1 by exists fM. have hf: A \Eq A1 by exists fA. pose p m := forall a, inc a A -> inc (J m a) M1. case: (all_exists_dichot2 p M); last first. move => [m mp pm]. have le1: A <=s M1. exists (Lf (fun z => J m z) A M1). by saw; apply: lf_injective => // u v _ _ /pr2_def. left; exact: (set_le_i2 le1 (EqS he)). move => hp. have hp1: forall m, inc m M -> exists2 a, inc a A & inc (J m a) A1. move => m mM; move:(hp _ mM) => pmm. case:(all_exists_dichot1 (fun a => inc (J m a) M1) A) => // - [a aA av]. move: (setXp_i mM aA); rewrite hc; case/setU2_P => // ok; ex_tac. pose phi m := the_least (induced_order r (Zo A (fun a => inc (J m a) A1))). have hg m: inc m M -> inc (J m (phi m)) A1. move => mM; rewrite /phi; set Z := Zo _ _. have sz: sub Z (substrate r) by rewrite osr; apply: Zo_S. have nez: nonempty Z. by move:(hp1 _ mM) => [a aa ab]; exists a; apply: Zo_i. move:(iorder_osr (proj1 wor) sz) =>[oZ sZ]. move: (proj1 (the_least_pr oZ (proj2 wor _ sz nez))). by rewrite sZ => /Zo_hi. have le1: M <=s A1. exists (Lf (fun m => (J m (phi m))) M A1). by saw; apply: lf_injective => // u v _ _ /pr1_def. right; exact: (set_le_i2 le1 (EqS hf)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)