proposition: Lemma finite_image_by f A: function f -> finite_set A -> finite_set (Vfs f A).
proof: Proof. move=> ff fsA; move:(image_smaller1 A ff) => cle. apply: (cle_fin_fin fsA cle). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)