proposition: Lemma Tarski_th1: (forall x y, Sinfinite x -> Sinfinite y -> x \times y \Eq dsum x y) -> proposition_Z.
proof: Proof. move => Hyp c ci; move: (proposition_S ci) => [pa pb pc]. exact: (Tarski_th1_aux ci pa pb pc (Hyp _ _ ci (proj1 pa))). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)