proposition: Lemma inj_source_smaller f: injection f -> (source f) <=cc (target f).
proof: Proof. move => injf; rewrite - (cardinal_range injf). apply:(sub_smaller (Imf_Starget (proj1 injf))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)