proposition: Lemma cardinal_image_injective : forall (E F : Setoid) (f : MAP E F) (A : part_set E) (n : nat), cardinal A n -> injective f -> cardinal (image f A) n.
proof: Proof. intros E F f A n H' H'0; try assumption. case (cardinal_image_lesser f H'). intros x H'1; try assumption. elim H'1; intros H'2 H'3; try exact H'2; clear H'1. cut (x < n \/ x = n). intros H'1; try assumption. elim H'1; [ intros H'4; try exact H'4; clear H'1 | intros H'4; clear H'1 ]. case (tiroirs (E:=E) (F:=F) (f:=f) (n:=n) (Chaussettes:=A) H' (m:=x) (Tiroirs:=image f A) H'2 H'4). auto with *. intros x0 H'1; try assumption. elim H'1; intros y E0; elim E0; intros H'5 H'6; try exact H'5; clear E0 H'1. red in H'0. absurd (Equal x0 y); auto with *. apply cardinal_comp with (image f A) x; auto with *. case (lt_eq_lt_dec x n). intros H'1; elim H'1; [ intros H'4; try exact H'4; clear H'1 | intros H'4; clear H'1 ]; auto with *. intros H'1; try assumption. absurd (n < x); auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec