proposition: Lemma injective_finite_inverse_image {X Y : Type} (f : X -> Y) (U : Ensemble Y) : injective f -> Finite U -> Finite (inverse_image f U).
proof: Proof. intros Hf HU. induction HU. { rewrite inverse_image_empty. constructor. } unfold Add. rewrite inverse_image_union. apply Union_preserves_Finite; auto. clear IHHU. apply injective_finite_inverse_image_Singleton. assumption. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)