proposition: Lemma Tarski_th5': (forall x y z, Sinfinite x -> Sinfinite y -> Sinfinite z -> x \times z <s y \times z -> x <s y)-> proposition_Z.
proof: Proof. move => hyp n ni. move: (proposition_S ni); set a := substrate _;move => [pa pb pc]. case:(p_or_not_p (n \Eq a)) => ean; first exact: (Saleph_inv pa (EqS ean)). move:(Eq_mul_mon1 n (Sinfinite_ne (proj1 pa))) => le1. move:(set_le_i2 (Eq_mul_mon1 a (Sinfinite_ne ni)) (Eq_setX2_S a n)) => le2. case: (p_or_not_p (a \Eq (n \times a))) => eq2. case: pb;split => //;exact:(set_le_i2 le1 (EqS eq2)). case: pc; apply:(hyp a n a (proj1 pa) ni (proj1 pa)). exact:(set_lt_i1 (conj le2 eq2) (Saleph_square pa)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)