proposition: Lemma finite_image f: function f -> finite_set (source f) -> finite_set (Imf f).
proof: Proof. move=> ff fs; move: (image_smaller ff)=> cle. apply: (cle_fin_fin fs cle). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)