proposition: Lemma Cantor_Bernstein2 f g: injection f -> injection g -> source f = target g -> source g = target f -> equipotent (source f)(source g).
proof: Proof. move => pa pb pc pd. move:(Cantor_Bernstein2_full pa pb pc pd). by set f0 := Lf _ _ _ => fp; exists f0. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)