proposition: Lemma map_not_injective : forall (A B : Setoid) (f : MAP A B) (n m : nat), cardinal (full A) n -> cardinal (full B) m -> m < n -> ~ injective f.
proof: Proof. intros A B f n m H' H'0 H'1; red in |- *; intros H'2; try exact H'2. red in H'2. case (tiroirs (E:=A) (F:=B) (f:=f) H' H'0 H'1); auto with *. intros x H'3; try assumption. elim H'3; intros y E; elim E; intros H'4 H'5; try exact H'4; clear E H'3; auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec