proposition: Lemma cardinal_complement_image f (S := source f) (T := target f) : injection f -> finite_set T -> cardinal (T -s (Imf f)) = (cardinal T) -c (cardinal S).
proof: Proof. move=> injf /NatP fb. have h:= (cardinal_complement_image1 injf). rewrite - h in fb |- *. have aN := (NS_in_sumr (CS_cardinal S) fb). have cN:= (NS_in_suml (CS_cardinal (T -s Imf f)) fb). by symmetry;apply: cdiff_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)