proposition: Lemma Tarski_th4': (forall x y z t, Sinfinite x -> Sinfinite y -> Sinfinite z -> Sinfinite t -> x <s y -> z <s t -> x \times z <s y \times t) -> proposition_Z.
proof: Proof. move => hyp m mi. have nse: nonempty Nat by exists \0c; apply: NS0. move:(Eq_pow_mon1 m nse). set n := functions _ _ => lmn. apply: (Saleph_mon mi lmn). have ni:= (Sinfinite_mon mi lmn). move: (proposition_S ni); set a := substrate _;move => [pa pb pc]. case:(p_or_not_p (a \Eq n)) => ean; first exact: (Saleph_inv pa ean). have nn: n \Eq (coarse n). move:(Eq_pow_inv (EqR m) (Saleph_double Saleph_Nat))(Eq_powpow m Nat C2). move => sa sb. exact:(EqT (EqT sa sb) (EqS (Eq_squareE n))). have ai := proj1 pa. move:(Eq_mul_mon1 n (Sinfinite_ne ai)) => le1. move:(set_le_i2 (Eq_mul_mon1 a (Sinfinite_ne ni)) (Eq_setX2_S a n)) => le2. case: (p_or_not_p (n \Eq (n \times a))) => eq1. case: pc; split => //; exact:(set_le_i2 le2 (EqS eq1)). case: (p_or_not_p (a \Eq (n \times a))) => eq2. by case: pb; split; [ exact:(set_le_i2 le1 (EqS eq2)) | move/EqS]. have pi:= (Sinfinite_mon ni le1). case:(proj2 (hyp _ _ _ _ ni pi (proj1 pa) pi (conj le1 eq1) (conj le2 eq2))). exact: (EqT (Eq_mul_inv nn (Saleph_square pa)) (EqS (Eq_square_mul n a))). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)