proposition: Lemma Tarski_th1_aux M A: Sinfinite M -> Saleph A -> ~ M <s A -> ~ A <s M -> M \times A \Eq dsum M A -> Saleph M.
proof: Proof. move => im pa pb pc res. case: (p_or_not_p (A \Eq M)) => eac. apply: (Saleph_inv pa eac). by case: (tarski_lemma1 pa res) => h; [case: pc | case: pb; split => // /EqS]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)