proposition: Lemma Saleph_double x: Saleph x -> x \Eq (x \times C2).
proof: Proof. move => h; move:(Saleph_square h) => a2. apply: CantorBernstein. have nec2: nonempty C2 by exists C0; apply: set2_1. exact: (Eq_mul_mon1 x nec2). exact: (set_le_i2 (Eq_mul_mon2 x (proj1 (set_lt_2inf (proj1 h)))) (EqS a2)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)