proposition: Lemma tiroirs : forall (n : nat) (Chaussettes : part_set E), cardinal Chaussettes n -> forall (m : nat) (Tiroirs : part_set F), cardinal Tiroirs m -> m < n -> (forall x : E, in_part x Chaussettes -> in_part (f x) Tiroirs) -> exists x : E, (exists y : E, ~ Equal x y /\ Equal (f x) (f y)).
proof: Proof. simple induction n. intros Chaussettes H' m Tiroirs H'0 H'1; try assumption. inversion H'1. intros n0 H' Chaussettes H'0 m Tiroirs H'1 H'2 H'3; try assumption. inversion H'0. elim (classic (ex (fun y : E => ~ Equal x y /\ Equal (Ap f x) (Ap f y)))); intros. exists x; try assumption. cut (exists m0 : nat, m = S m0). intros H'4; try assumption. case H'4; clear H'4; intros. apply H' with (diff Chaussettes (single x)) x0 (diff Tiroirs (single (f x))). apply cardinal_S with Chaussettes x. unfold not in |- *; intros. absurd (~ in_part x (single x)); auto with *. apply diff_in_r with Chaussettes; auto with *. auto with *. apply diff_add_part2. apply in_part_comp_r with (add_part B x); auto with *. auto with *. apply cardinal_minus_part. rewrite <- H5; auto with *. apply H'3; auto with *. apply in_part_comp_r with (add_part B x). auto with *. auto with *. rewrite H5 in H'2; auto with *. intros x1 H'4; try assumption. apply in_diff. apply H'3; auto with *. apply diff_in_l with (single x); auto with *. unfold not in |- *; intros. unfold not in H4. apply H4. exists x1; try assumption. split. intros H'5; try assumption. cut (~ in_part x1 (single x)). intro. apply H7. apply in_part_trans_eq with x; auto with *. apply diff_in_r with Chaussettes; auto with *. auto with *. inversion H'1. cut (in_part (f x) Tiroirs). intros H'4; try assumption. absurd (in_part (f x) (empty F)); auto with *. apply in_part_comp_r with Tiroirs; auto with *. apply H'3. apply in_part_comp_r with (add_part B x); auto with *. exists n2; try assumption. auto with *. Qed.
imports: Fpart2