proposition: Lemma Tarski_th5: (forall x y z, Sinfinite x -> Sinfinite y -> Sinfinite z -> dsum x z <s dsum y 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_sum_mono1 n a) (Eq_sum_mono1_bis n a) => le1 le2. case: (p_or_not_p (a \Eq (dsum n a))) => eq1. case: pb; split => //;exact:(set_le_i2 le1 (EqS eq1)). case: pc; apply:(hyp a n a (proj1 pa) ni (proj1 pa));rewrite(dsum_same a). exact:(set_lt_i1 (conj le2 eq1) (Saleph_double pa)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)