proposition: Lemma not_injective_prop : forall (A B : Setoid) (f : MAP A B), ~ injective f -> exists x : A, (exists y : A, ~ Equal x y /\ Equal (f x) (f y)).
proof: Proof. unfold injective in |- *. intros A B f H'; try assumption. cut (ex (fun x : A => ~ (forall y : A, ~ (~ Equal x y /\ Equal (Ap f x) (Ap f y))))). intros H'0; try assumption. elim H'0; intros x E; try exact E; clear H'0. exists x; try assumption. cut (ex (fun y : A => ~ ~ (~ Equal x y /\ Equal (Ap f x) (Ap f y)))). intros H'0; try assumption. elim H'0; intros y E0; try exact E0; clear H'0. exists y; try assumption. apply NNPP; auto with *. apply not_all_ex_not with (P := fun y : A => ~ (~ Equal x y /\ Equal (Ap f x) (Ap f y))); auto with *. apply not_all_ex_not with (P := fun x : A => forall y : A, ~ (~ Equal x y /\ Equal (Ap f x) (Ap f y))); auto with *. red in |- *. intros H'0; try assumption. apply H'. intros x y H'1; try assumption. specialize H'0 with (n := x) (y := y); rename H'0 into H'3; try exact H'3. apply NNPP; tauto. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec