proposition: Lemma infinite_compl A B: infinite_set B -> cardinal A <c cardinal B -> cardinal (B -s A) = cardinal B.
proof: Proof. move => /infinite_setP p1 p2. ex_middle nsc. move: (csum2_pr6_inf2 p1 p2 (conj (sub_smaller (@sub_setC B A)) nsc)). by rewrite setU2Cr2; move: (sub_smaller (@subsetU2r A B)) => /cleNgt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)