proposition: Lemma sub_image_finite_set A B f: finite_set B -> (forall x, inc x A -> inc (f x) B) -> {inc A &, injective f} -> finite_set A.
proof: Proof. move => fsb fa fb. have h: injection (Lf f A B) by apply: lf_injective. by move:(inj_source_smaller h); aw; apply: cle_fin_fin. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)