proposition: Lemma not_injective_elim : forall f:U -> V, ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y).
proof: Proof. unfold injective; intros f H. cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)). 2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y); trivial with sets. destruct 1 as [x C]; exists x. cut (exists y : _, ~ (f x = f y -> x = y)). 2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y); trivial with sets. destruct 1 as [y D]; exists y. apply imply_to_and; trivial with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts