proposition: Lemma cardinal_image_strict_lesser : forall (E F : Setoid) (f : MAP E F) (n : nat), cardinal (full E) n -> ~ injective f -> exists m : nat, cardinal (image_map f) m /\ m < n.
proof: Proof. intros E F f n; try assumption. case n. intros H' H'0; try assumption. case (not_injective_prop H'0). intros x H'1; try assumption. absurd (in_part x (full E)); auto with *. apply not_in_part_comp_r with (empty E); auto with *. inversion H'. auto with *. intros n0 H' H'0; try assumption. case (not_injective_prop H'0). intros x H'1; try assumption. elim H'1; intros y E0; elim E0; intros H'2 H'3; try exact H'2; clear E0 H'1. cut (cardinal (diff (full E) (single x)) n0). intros H'1; try assumption. case (cardinal_image_lesser f H'1). intros m H'4; try assumption. exists m; split; [ try assumption | idtac ]. elim H'4; intros H'5 H'6; try exact H'5; clear H'4. apply cardinal_comp with (image f (diff (full E) (single x))) m; auto with *. apply included_antisym. unfold image_map in |- *. apply image_included; auto with *. unfold image_map in |- *. unfold included in |- *. intros x0 H'4; try assumption. elim H'4. intros x1 H'7; try assumption. case (classic (Equal x1 x)). intros H'8; try assumption. simpl in |- *. exists y; split; [ idtac | try assumption ]. split; [ idtac | try assumption ]. auto with *. auto with *. apply Trans with (f x); auto with *. elim H'7; intros H'9 H'10; try exact H'10; clear H'7. apply Trans with (f x1); auto with *. intros H'8; try assumption. simpl in |- *. exists x1; split; [ idtac | try assumption ]. auto with *. elim H'7; intros H'9 H'10; try exact H'10; clear H'7. elim H'4; intros H'5 H'6; try exact H'6; clear H'4; auto with *. apply cardinal_S with (full E) x; auto with *. unfold add_part in |- *. auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec