proposition: Lemma cardinal_complement_image1 f (S := source f) (T := target f) : injection f -> (cardinal (T -s (Imf f))) +c (cardinal S) = cardinal T.
proof: Proof. move => injf. set A:= (Imf f). have ->: (cardinal S = cardinal A). apply /card_eqP;exists (restriction_to_image f). rewrite /restriction_to_image/restriction2; hnf;saw. by apply: (restriction_to_image_fb injf). symmetry; rewrite csumC. have p0: sub A T by apply: Imf_Starget; fct_tac. rewrite - {1} (setU2_Cr p0) csum2cl csum2cr csum2_pr5 //;apply: set_I2Cr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)