proposition: Lemma Pigeonhole_principle : forall (A:Ensemble U) (f:U -> V) (n:nat), cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y).
proof: Proof. intros; apply not_injective_elim. apply Pigeonhole with A n n'; trivial with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts