proposition: Theorem Pigeonhole : forall (A:Ensemble U) (f:U -> V) (n:nat), cardinal U A n -> forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
proof: Proof. unfold not; intros A f n CAn n' CIfn' ltn'n I. cut (n' = n). - intro E; generalize ltn'n; rewrite E; exact (Nat.lt_irrefl n). - apply injective_preserves_cardinal with (A := A) (f := f) (n := n); trivial with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts