proposition: Lemma not_surjective_prop : forall (A B : Setoid) (f : MAP A B), ~ surjective f -> exists y : B, ~ in_part y (image_map f).
proof: Proof. intros A B f H'; try assumption. apply not_all_ex_not with (P := fun y : B => in_part y (image_map f)). red in |- *. red in H'. intros H'0; try assumption. lapply H'; [ intros H'1; try exact H'1; clear H' | clear H' ]. red in |- *. simpl in H'0. intros y; try assumption. elim (H'0 y); intros x E; elim E; intros H'1 H'2; try exact H'2; clear E. exists x; try assumption. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec