proposition: Lemma Finite_injective_image {X Y : Type} (f : X -> Y) (U : Ensemble X) : injective_ens f U -> Finite (Im U f) -> Finite U.
proof: Proof. intros Hf Himg. apply Finite_injective_image_dec with f; auto. intros ? ? ? ?. apply classic. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)