proposition: Theorem Pigeonhole_ter : forall (A:Ensemble U) (f:U -> V) (n:nat), injective U V f -> Finite V (Im U V A f) -> Finite U A.
proof: Proof. intros A f H' H'0 H'1. apply NNPP. red; intro H'2. elim (Pigeonhole_bis A f); auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image