proposition: Lemma cardinal_image_equal_injective : forall (E F : Setoid) (f : MAP E F) (n : nat), cardinal (full E) n -> cardinal (image_map f) n -> injective f.
proof: Proof. intros E F f n H' H'0; try assumption. apply NNPP. red in |- *; intros H'1; try exact H'1. case (cardinal_image_strict_lesser H' H'1). intros x H'2; elim H'2; intros H'3 H'4; try exact H'4; clear H'2. absurd (x = n); auto with *. red in |- *; intros H'2; try exact H'2. absurd (x < n); auto with *. rewrite H'2. auto with *. apply cardinal_unique with (E := F) (A := image_map f); auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec