proposition: Lemma Tarski_th2: (forall x, Sinfinite x -> coarse x \Eq x) -> proposition_Z.
proof: Proof. move => H; apply: Tarski_th1 => x y xi yi. have zi := (H _ (Sinfinite_mon xi (Eq_sum_mono1 x y))). apply:set_leA; first exact:(set_le_i2 (set_le_ab_sab2 x y) zi). move:(proj1 (set_lt_2inf xi)) (proj1 (set_lt_2inf yi)) => xs ys. by apply:set_le_ab_sab. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)