proposition: Lemma Tarski_th4: (forall x y z t, Sinfinite x -> Sinfinite y -> Sinfinite z -> Sinfinite t -> x <s y -> z <s t -> (dsum x z) <s (dsum y t)) -> proposition_Z.
proof: Proof. move => hyp m mi. have nse: nonempty Nat by exists \0c; apply: NS0. move: (Eq_mul_mon1 m nse); set n := product _ _ => lmn. have ni:= (Sinfinite_mon mi lmn). move: (proposition_S ni); set a := substrate _;move => [pa pb pc]. apply: (Saleph_mon mi lmn). case:(p_or_not_p (a \Eq n)) => ean; first exact: (Saleph_inv pa ean). move: (Eq_sum_mono1 n a) (Eq_sum_mono1_bis n a) => le1 le2. case: (p_or_not_p (n \Eq (dsum n a))) => eq1. case: pc; split => //; exact:(set_le_i2 le2 (EqS eq1)). case: (p_or_not_p (a \Eq (dsum n 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))). move:(Saleph_double pa) => aa. move:(EqT (Eq_mul_inv (EqR m) (Saleph_double Saleph_Nat)) (Eq_mulA m Nat C2)). rewrite -/ n => nn. rewrite dsum_same. exact: (EqT (Eq_sum_inv nn aa) (EqS (Eq_muldl C2 n a))). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)