proposition: Lemma Tarski_th3: (forall x y, Sinfinite x -> Sinfinite y -> (coarse x) \Eq (coarse y) -> x \Eq y) -> 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]. pose p := dsum n a; pose q := n \times a. have ai := (proj1 pa). have nea:= (Sinfinite_ne ai). have lenp: n <=s p by apply: Eq_sum_mono1. have lenq: n <=s q by apply:(Eq_mul_mon1 _ nea). move: (Sinfinite_mon ni lenp) (Sinfinite_mon ni lenq) => pi qi. apply:(Tarski_th1_aux ni pa pb pc); apply: EqS; apply:(hyp p q pi qi). 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))). move: (Saleph_square pa)(Saleph_double pa) => sa da. have sq: coarse q \Eq q. exact :(EqT (Eq_square_mul n a) (Eq_mul_inv (EqS nn) (EqS sa))). have dq: q \times C2 \Eq q. exact: (EqT (EqS (Eq_mulA n a C2)) (Eq_mul_inv (EqR n) (EqS da))). have lpq: p <=s q. move:(proj1 (set_lt_2inf ni)) (proj1 (set_lt_2inf ai)) => nl al. exact:(set_le_ab_sab nl al). have eq1: dsum p q \Eq q. apply: set_leA; last exact: (set_le_i2 (Eq_sum_mono1 q p) (Eq_sumC q p)). move: (Eq_sum_mono2 q lpq); rewrite dsum_same => h. exact: (set_le_i2 h dq). move:(EqT (Eq_add_square n a) (EqS (Eq_sum_inv (Eq_sum_inv nn sa) (EqS dq)))). move=> h; exact:(EqT (EqT h eq1) (EqS sq)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)