proposition: Theorem CantorBernstein X Y: X <=s Y -> Y <=s X -> X \Eq Y.
proof: Proof. move=> [f fa][g gb]. move: (CantorBernstein_eff fa gb) =>h. by exists (cantor_bernstein_bij X Y f g). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)