(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Tiroirs.
Require Export Parts2.
Require Export Classical_Pred_Type.
Require Export Compare_dec.

Lemma not_injective_prop :
 forall (A B : Setoid) (f : MAP A B),
 ~ injective f ->
 exists x : A, (exists y : A, ~ Equal x y /\ Equal (f x) (f y)).
(* Goal: forall (A B : Setoid) (f : Carrier (MAP A B)) (_ : not (@injective A B f)), @ex (Carrier A) (fun x : Carrier A => @ex (Carrier A) (fun y : Carrier A => and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y)))) *)
unfold injective in |- *.
(* Goal: forall (A B : Setoid) (f : Carrier (MAP A B)) (_ : not (@surjective A B f)), @ex (Carrier B) (fun y : Carrier B => not (@in_part B y (@image_map A B f))) *)
intros A B f H'; try assumption.
cut
 (ex
    (fun x : A =>
     ~ (forall y : A, ~ (~ Equal x y /\ Equal (Ap f x) (Ap f y))))).
(* Goal: forall _ : forall n : Carrier B, @in_part B n (@image_map A B f), False *)
intros H'0; try assumption.
(* Goal: @ex (Carrier A) (fun x : Carrier A => @ex (Carrier A) (fun y : Carrier A => and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y)))) *)
(* Goal: @ex (Carrier A) (fun x : Carrier A => not (forall y : Carrier A, not (and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))))) *)
elim H'0; intros x E; try exact E; clear H'0.
(* Goal: @ex (Carrier A) (fun x : Carrier A => @Equal B y (@Ap A B f x)) *)
exists x; try assumption.
(* Goal: @ex (Carrier A) (fun y : Carrier A => and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))) *)
(* Goal: @ex (Carrier A) (fun x : Carrier A => not (forall y : Carrier A, not (and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))))) *)
cut (ex (fun y : A => ~ ~ (~ Equal x y /\ Equal (Ap f x) (Ap f y)))).
(* Goal: forall _ : forall n : Carrier B, @in_part B n (@image_map A B f), False *)
intros H'0; try assumption.
(* Goal: @ex (Carrier A) (fun y : Carrier A => and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))) *)
(* Goal: @ex (Carrier A) (fun y : Carrier A => not (not (and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))))) *)
(* Goal: @ex (Carrier A) (fun x : Carrier A => not (forall y : Carrier A, not (and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))))) *)
elim H'0; intros y E0; try exact E0; clear H'0.
(* Goal: @ex (Carrier A) (fun y : Carrier A => and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))) *)
(* Goal: @ex (Carrier A) (fun y : Carrier A => not (not (and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))))) *)
(* Goal: @ex (Carrier A) (fun x : Carrier A => not (forall y : Carrier A, not (and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))))) *)
exists y; try assumption.
(* Goal: and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y)) *)
(* Goal: @ex (Carrier A) (fun y : Carrier A => not (not (and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))))) *)
(* Goal: @ex (Carrier A) (fun x : Carrier A => not (forall y : Carrier A, not (and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y))))) *)
apply NNPP; auto with *.
apply
 not_all_ex_not
  with (P := fun y : A => ~ (~ Equal x y /\ Equal (Ap f x) (Ap f y)));
(* Goal: @cardinal E A n *)
 auto with *.
apply
 not_all_ex_not
  with
    (P := fun x : A =>
          forall y : A, ~ (~ Equal x y /\ Equal (Ap f x) (Ap f y)));
(* Goal: @cardinal E A n *)
 auto with *.
(* Goal: not (@Equal E x1 x0) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
red in |- *.
(* Goal: forall _ : forall n : Carrier B, @in_part B n (@image_map A B f), False *)
intros H'0; try assumption.
(* Goal: False *)
apply H'.
(* Goal: forall (x y : Carrier A) (_ : @Equal B (@Ap A B f x) (@Ap A B f y)), @Equal A x y *)
intros x y H'1; try assumption.
specialize  H'0 with (n := x) (y := y); rename H'0 into H'3; try exact H'3.
(* Goal: @Equal A x y *)
apply NNPP; tauto.
Qed.

Lemma not_surjective_prop :
 forall (A B : Setoid) (f : MAP A B),
 ~ surjective f -> exists y : B, ~ in_part y (image_map f).
(* Goal: forall (A B : Setoid) (f : Carrier (MAP A B)) (_ : not (@surjective A B f)), @ex (Carrier B) (fun y : Carrier B => not (@in_part B y (@image_map A B f))) *)
intros A B f H'; try assumption.
(* Goal: @ex (Carrier B) (fun y : Carrier B => not (@in_part B y (@image_map A B f))) *)
apply not_all_ex_not with (P := fun y : B => in_part y (image_map f)).
(* Goal: not (@Equal E x1 x0) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
red in |- *.
(* Goal: forall _ : forall n : Carrier B, @in_part B n (@image_map A B f), False *)
red in H'.
(* Goal: forall _ : forall n : Carrier B, @in_part B n (@image_map A B f), False *)
intros H'0; try assumption.
(* Goal: False *)
lapply H'; [ intros H'1; try exact H'1; clear H' | clear H' ].
(* Goal: not (@Equal E x1 x0) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
red in |- *.
(* Goal: forall y : Carrier B, @ex (Carrier A) (fun x : Carrier A => @Equal B y (@Ap A B f x)) *)
simpl in H'0.
(* Goal: forall y : Carrier B, @ex (Carrier A) (fun x : Carrier A => @Equal B y (@Ap A B f x)) *)
intros y; try assumption.
(* Goal: @ex (Carrier A) (fun x : Carrier A => @Equal B y (@Ap A B f x)) *)
elim (H'0 y); intros x E; elim E; intros H'1 H'2; try exact H'2; clear E.
(* Goal: @ex (Carrier A) (fun x : Carrier A => @Equal B y (@Ap A B f x)) *)
exists x; try assumption.
Qed.
Parameter
  image_empty :
    forall (E F : Setoid) (f : MAP E F) (A : part_set E),
    Equal A (empty E) -> Equal (image f A) (empty F).
Hint Resolve image_empty: algebra.
Parameter
  image_union :
    forall (E F : Setoid) (f : MAP E F) (A B : part_set E),
    Equal (image f (union A B)) (union (image f A) (image f B)).
Hint Resolve image_union: algebra.
Parameter
  image_single :
    forall (E F : Setoid) (f : MAP E F) (A : part_set E) (x : E),
    Equal (image f (single x)) (single (f x)).
Hint Resolve image_single: algebra.
Parameter
  union_single_in :
    forall (E : Setoid) (A : part_set E) (x : E),
    in_part x A -> Equal (union A (single x)) A.
Hint Resolve union_single_in: algebra.

Lemma cardinal_image_lesser :
 forall (E F : Setoid) (f : MAP E F) (A : part_set E) (n : nat),
 cardinal A n -> exists m : nat, cardinal (image f A) m /\ m <= n.
(* Goal: forall (E F : Setoid) (f : Carrier (MAP E F)) (A : Carrier (part_set E)) (n : nat) (_ : @cardinal E A n), @ex nat (fun m : nat => and (@cardinal F (@image E F f A) m) (le m n)) *)
intros E F f A n H'; try assumption.
apply
 cardinal_ind2
  with
    (P := fun (n : nat) (A : part_set E) (c : cardinal A n) =>
          ex (fun m : nat => cardinal (image f A) m /\ m <= n)).
(* Goal: forall (A : Carrier (part_set E)) (_ : @cardinal E A O), @ex nat (fun m : nat => and (@cardinal F (@image E F f A) m) (le m O)) *)
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : @cardinal E B n), @ex nat (fun m : nat => and (@cardinal F (@image E F f B) m) (le m n))) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (@add_part E B x)) (_ : @cardinal E A (S n)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A) m) (le m (S n))) *)
(* Goal: @cardinal E A n *)
intros A0 H'0; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m O)) *)
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : @cardinal E B n), @ex nat (fun m : nat => and (@cardinal F (@image E F f B) m) (le m n))) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (@add_part E B x)) (_ : @cardinal E A (S n)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A) m) (le m (S n))) *)
(* Goal: @cardinal E A n *)
exists 0; split; [ idtac | auto with * ].
(* Goal: @cardinal F (@image E F f A0) O *)
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : @cardinal E B n), @ex nat (fun m : nat => and (@cardinal F (@image E F f B) m) (le m n))) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (@add_part E B x)) (_ : @cardinal E A (S n)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A) m) (le m (S n))) *)
(* Goal: @cardinal E A n *)
apply cardinal_empty; auto with *.
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : @cardinal E B n), @ex nat (fun m : nat => and (@cardinal F (@image E F f B) m) (le m n))) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (@add_part E B x)) (_ : @cardinal E A (S n)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A) m) (le m (S n))) *)
(* Goal: @cardinal E A n *)
intros n0 H'0 A0 B x H'1 H'2 H'3; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
case (classic (in_part (f x) (image f B))).
(* Goal: forall _ : not (@in_part F (@Ap E F f x) (@image E F f B)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
intros H'4; try assumption.
elim (H'0 B);
 [ intros m E0; elim E0; intros H'7 H'8; try exact H'7; clear E0 | idtac ].
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E B n0 *)
(* Goal: forall _ : not (@in_part F (@Ap E F f x) (@image E F f B)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
exists m; split; [ idtac | try assumption ].
(* Goal: @cardinal F (@image E F f A0) m *)
(* Goal: le m (S n0) *)
(* Goal: @cardinal E B n0 *)
(* Goal: forall _ : not (@in_part F (@Ap E F f x) (@image E F f B)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
apply cardinal_comp with (image f B) m; auto with *.
(* Goal: @Equal (part_set E) A0 (@add_part E (@minus_part E A0 x0) x0) *)
(* Goal: @cardinal E A n *)
apply Sym.
(* Goal: @Equal (part_set F) (@image E F f A0) (@image E F f B) *)
(* Goal: le m (S n0) *)
(* Goal: @cardinal E B n0 *)
(* Goal: forall _ : not (@in_part F (@Ap E F f x) (@image E F f B)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
apply Trans with (image f (add_part B x)); auto with *.
(* Goal: @Equal (part_set E) (full E) (@add_part E (@diff E (full E) (@single E x)) x) *)
unfold add_part in |- *.
(* Goal: @Equal (part_set F) (@image E F f (@union E B (@single E x))) (@union F (@image E F f B) (@single F (@Ap E F f x))) *)
(* Goal: le (S m) (S n0) *)
(* Goal: @cardinal E B n0 *)
(* Goal: @cardinal E A n *)
apply Trans with (union (image f B) (image f (single x))); auto with *.
(* Goal: @Equal (part_set F) (@union F (@image E F f B) (@image E F f (@single E x))) (@image E F f B) *)
(* Goal: le m (S n0) *)
(* Goal: @cardinal E B n0 *)
(* Goal: forall _ : not (@in_part F (@Ap E F f x) (@image E F f B)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
apply Trans with (union (image f B) (single (Ap f x))); auto with *.
(* Goal: @cardinal E A n *)
auto with *.
(* Goal: @cardinal E A n *)
apply cardinal_S with A0 x; auto with *.
(* Goal: forall _ : not (@in_part F (@Ap E F f x) (@image E F f B)), @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
intros H'4; try assumption.
elim (H'0 B);
 [ intros m E0; elim E0; intros H'7 H'8; try exact H'7; clear E0 | idtac ].
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image E F f A0) m) (le m (S n0))) *)
(* Goal: @cardinal E B n0 *)
(* Goal: @cardinal E A n *)
exists (S m); split; [ try assumption | idtac ].
(* Goal: @cardinal E A n *)
apply cardinal_add with (image f B) (Ap f x); auto with *.
(* Goal: @Equal (part_set E) (full E) (@add_part E (@diff E (full E) (@single E x)) x) *)
unfold add_part in |- *.
(* Goal: @Equal (part_set F) (@image E F f A0) (@union F (@image E F f B) (@single F (@Ap E F f x))) *)
(* Goal: le (S m) (S n0) *)
(* Goal: @cardinal E B n0 *)
(* Goal: @cardinal E A n *)
unfold add_part in H'2.
(* Goal: @cardinal E A n *)
apply Trans with (image f (union B (single x))); auto with *.
(* Goal: @Equal (part_set F) (@image E F f (@union E B (@single E x))) (@union F (@image E F f B) (@single F (@Ap E F f x))) *)
(* Goal: le (S m) (S n0) *)
(* Goal: @cardinal E B n0 *)
(* Goal: @cardinal E A n *)
apply Trans with (union (image f B) (image f (single x))); auto with *.
(* Goal: @cardinal E A n *)
auto with *.
(* Goal: @cardinal E A n *)
apply cardinal_S with A0 x; auto with *.
(* Goal: @cardinal E A n *)
auto with *.
Qed.

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.
intros E F f A n H' H'0; try assumption.
case (cardinal_image_lesser f H').
(* Goal: forall (x : Carrier E) (_ : @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))), @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
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).
(* Goal: forall _ : @in_part E x B, False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
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).
(* Goal: @cardinal E A n *)
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.
(* Goal: @cardinal E A n *)
absurd (Equal x0 y); auto with *.
(* Goal: @cardinal E A n *)
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 ];
(* Goal: @cardinal E A n *)
 auto with *.
(* Goal: forall _ : @in_part E x B, False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
intros H'1; try assumption.
(* Goal: @cardinal E A n *)
absurd (n < x); auto with *.
Qed.
Parameter
  not_in_part_comp_r :
    forall (E : Setoid) (A B : part_set E) (x : E),
    ~ in_part x A -> Equal A B -> ~ in_part x B.
Parameter
  diff_single_not_in :
    forall (E : Setoid) (A : part_set E) (x : E),
    ~ in_part x (diff A (single x)).
Hint Resolve diff_single_not_in: algebra.
Parameter
  diff_el_union_single :
    forall (E : Setoid) (A : part_set E) (x : E),
    in_part x A -> Equal A (union (diff A (single x)) (single x)).
Hint Resolve diff_el_union_single: algebra.

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.
(* Goal: forall (E F : Setoid) (f : Carrier (MAP E F)) (n : nat) (_ : @cardinal E (full E) n) (_ : not (@injective E F f)), @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m n)) *)
intros E F f n; try assumption.
(* Goal: forall (_ : @cardinal E (full E) n) (_ : not (@injective E F f)), @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m n)) *)
case n.
(* Goal: forall (_ : @included E B A) (_ : not (forall x : Carrier E, and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))), @ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (not (@in_part E x B))) *)
intros H' H'0; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
case (not_injective_prop H'0).
(* Goal: forall (x : Carrier E) (_ : @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))), @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
intros x H'1; try assumption.
(* Goal: @cardinal E A n *)
absurd (in_part x (full E)); auto with *.
(* Goal: @cardinal E A n *)
apply not_in_part_comp_r with (empty E); auto with *.
(* Goal: @Equal (part_set E) (empty E) (full E) *)
(* Goal: forall (n : nat) (_ : @cardinal E (full E) (S n)) (_ : not (@injective E F f)), @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n))) *)
inversion H'.
(* Goal: @cardinal E A n *)
auto with *.
(* Goal: forall (n : nat) (_ : @cardinal E (full E) (S n)) (_ : not (@injective E F f)), @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n))) *)
intros n0 H' H'0; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
case (not_injective_prop H'0).
(* Goal: forall (x : Carrier E) (_ : @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))), @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
intros x H'1; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
elim H'1; intros y E0; elim E0; intros H'2 H'3; try exact H'2; clear E0 H'1.
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
cut (cardinal (diff (full E) (single x)) n0).
(* Goal: forall _ : @in_part E x B, False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
intros H'1; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
case (cardinal_image_lesser f H'1).
(* Goal: forall (x0 : nat) (_ : and (@cardinal F (@image E F f (@diff E (full E) (@single E x))) x0) (le x0 n0)), @ex nat (fun m : nat => and (@cardinal F (@image_map E F f) m) (lt m (S n0))) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
intros m H'4; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n0))) *)
(* Goal: @included E B0 (@minus_part E A0 x0) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
exists m; split; [ try assumption | idtac ].
(* Goal: @cardinal F (@image_map E F f) m *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
elim H'4; intros H'5 H'6; try exact H'5; clear H'4.
(* Goal: @cardinal E A n *)
apply cardinal_comp with (image f (diff (full E) (single x))) m; auto with *.
(* Goal: @Equal (part_set F) (@image E F f (@diff E (full E) (@single E x))) (@image_map E F f) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
apply included_antisym.
(* Goal: @Equal (part_set F) (@image_map E F f) (full F) *)
unfold image_map in |- *.
(* Goal: @cardinal E A n *)
apply image_included; auto with *.
(* Goal: @Equal (part_set F) (@image_map E F f) (full F) *)
unfold image_map in |- *.
(* Goal: @included F (@image E F f (full E)) (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
unfold included in |- *.
(* Goal: forall (x0 : Carrier F) (_ : @in_part F x0 (@image E F f (full E))), @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
intros x0 H'4; try assumption.
(* Goal: @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
elim H'4.
(* Goal: forall (x1 : Carrier E) (_ : and (@in_part E x1 (full E)) (@Equal F x0 (@Ap E F f x1))), @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
intros x1 H'7; try assumption.
(* Goal: @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
case (classic (Equal x1 x)).
(* Goal: forall _ : not (@Equal E x1 x), @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
intros H'8; try assumption.
(* Goal: @in_part E x1 (@diff E A0 (@single E x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
simpl in |- *.
(* Goal: @ex (Carrier E) (fun x1 : Carrier E => and (and True (not (@Equal E x1 x))) (@Equal F x0 (@Ap E F f x1))) *)
(* Goal: forall _ : not (@Equal E x1 x), @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
exists y; split; [ idtac | try assumption ].
(* Goal: and True (not (@Equal E y x)) *)
(* Goal: @Equal F x0 (@Ap E F f y) *)
(* Goal: forall _ : not (@Equal E x1 x), @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
split; [ idtac | try assumption ].
(* Goal: @cardinal E A n *)
auto with *.
(* Goal: @cardinal E A n *)
auto with *.
(* Goal: @cardinal E A n *)
apply Trans with (f x); auto with *.
(* Goal: @Equal F x0 (@Ap E F f x1) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
elim H'7; intros H'9 H'10; try exact H'10; clear H'7.
(* Goal: @cardinal E A n *)
apply Trans with (f x1); auto with *.
(* Goal: forall _ : not (@Equal E x1 x), @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
intros H'8; try assumption.
(* Goal: @in_part E x1 (@diff E A0 (@single E x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
simpl in |- *.
(* Goal: and True (not (@Equal E y x)) *)
(* Goal: @Equal F x0 (@Ap E F f y) *)
(* Goal: forall _ : not (@Equal E x1 x), @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
exists x1; split; [ idtac | try assumption ].
(* Goal: @cardinal E A n *)
auto with *.
(* Goal: @Equal F x0 (@Ap E F f x1) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
elim H'7; intros H'9 H'10; try exact H'10; clear H'7.
(* Goal: @cardinal E A n *)
elim H'4; intros H'5 H'6; try exact H'6; clear H'4; auto with *.
(* Goal: @cardinal E A n *)
apply cardinal_S with (full E) x; auto with *.
(* Goal: @Equal (part_set E) (full E) (@add_part E (@diff E (full E) (@single E x)) x) *)
unfold add_part in |- *.
(* Goal: @cardinal E A n *)
auto with *.
Qed.

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.
(* Goal: forall (E F : Setoid) (f : Carrier (MAP E F)) (n : nat) (_ : @cardinal E (full E) n) (_ : @cardinal F (@image_map E F f) n), @injective E F f *)
intros E F f n H' H'0; try assumption.
(* Goal: @in_part E x A *)
(* Goal: not (@in_part E x B) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
apply NNPP.
(* Goal: not (not (@in_part E x A)) *)
(* Goal: not (@in_part E x B) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
red in |- *; intros H'1; try exact H'1.
(* Goal: False *)
case (cardinal_image_strict_lesser H' H'1).
(* Goal: forall (x : nat) (_ : and (@cardinal F (@image_map E F f) x) (lt x n)), False *)
intros x H'2; elim H'2; intros H'3 H'4; try exact H'4; clear H'2.
(* Goal: @cardinal E A n *)
absurd (x = n); auto with *.
(* Goal: not (@eq nat x n) *)
(* Goal: @eq nat x n *)
red in |- *; intros H'2; try exact H'2.
(* Goal: @cardinal E A n *)
absurd (x < n); auto with *.
(* Goal: not (lt x n) *)
(* Goal: @eq nat x n *)
rewrite H'2.
(* Goal: @cardinal E A n *)
auto with *.
(* Goal: @cardinal E A n *)
apply cardinal_unique with (E := F) (A := image_map f); auto with *.
Qed.
Parameter
  cardinal_equal_included_equal :
    forall (E : Setoid) (A B : part_set E) (n : nat),
    cardinal A n -> cardinal B n -> included B A -> Equal B A.
Parameter
  image_full_surjective :
    forall (E F : Setoid) (f : MAP E F),
    Equal (image_map f) (full F) -> surjective f.
Hint Resolve image_full_surjective: algebra.

Lemma finite_injective_surjective :
 forall (E F : Setoid) (f : MAP E F) (n : nat),
 cardinal (full E) n -> cardinal (full F) n -> injective f -> surjective f.
(* Goal: forall (E F : Setoid) (f : Carrier (MAP E F)) (n : nat) (_ : @cardinal E (full E) n) (_ : @cardinal F (full F) n) (_ : @surjective E F f), @injective E F f *)
intros E F f n H' H'0 H'1; try assumption.
(* Goal: @surjective E F f *)
generalize (cardinal_image_injective H' H'1).
(* Goal: forall _ : @in_part E x B, @in_part E x A *)
(* Goal: forall _ : @in_part E x A, @in_part E x B *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
intros H'2; try assumption.
(* Goal: @cardinal E A n *)
apply image_full_surjective; auto with *.
(* Goal: @Equal (part_set F) (@image_map E F f) (full F) *)
unfold image_map in |- *.
(* Goal: @cardinal E A n *)
apply cardinal_equal_included_equal with n; auto with *.
Qed.
Parameter
  surjective_image_full :
    forall (E F : Setoid) (f : MAP E F),
    surjective f -> Equal (image_map f) (full F).
Hint Resolve surjective_image_full: algebra.

Lemma finite_surjective_injective :
 forall (E F : Setoid) (f : MAP E F) (n : nat),
 cardinal (full E) n -> cardinal (full F) n -> surjective f -> injective f.
(* Goal: forall (E F : Setoid) (f : Carrier (MAP E F)) (n : nat) (_ : @cardinal E (full E) n) (_ : @cardinal F (full F) n) (_ : @surjective E F f), @injective E F f *)
intros E F f n H' H'0 H'1; try assumption.
(* Goal: @cardinal E A n *)
apply cardinal_image_equal_injective with n; auto with *.
(* Goal: @cardinal E A n *)
apply cardinal_comp with (full F) n; auto with *.
(* Goal: @cardinal E A n *)
apply Sym; auto with *.
Qed.

Lemma not_included_exist :
 forall (E : Setoid) (A B : part_set E),
 included B A -> ~ Equal B A -> exists x : E, in_part x A /\ ~ in_part x B.
(* Goal: @in_part E x1 (@diff E A0 (@single E x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
intros E A B; simpl in |- *.
(* Goal: @in_part E x1 (@diff E A0 (@single E x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
unfold eq_part in |- *; simpl in |- *.
(* Goal: forall (_ : @included E B A) (_ : not (forall x : Carrier E, and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))), @ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (not (@in_part E x B))) *)
intros H' H'0; try assumption.
cut
 (ex
    (fun x : E =>
     ~ ((in_part x B -> in_part x A) /\ (in_part x A -> in_part x B)))).
(* Goal: forall _ : @in_part E x B, False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
intros H'1; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (not (@in_part E x B))) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
elim H'1; intros x E0; try exact E0; clear H'1.
(* Goal: @ex (Carrier E) (fun x : Carrier E => and (@in_part E x A) (not (@in_part E x B))) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
exists x; split; [ try assumption | idtac ].
(* Goal: forall _ : @in_part E x B, False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
red in E0.
(* Goal: @in_part E x A *)
(* Goal: not (@in_part E x B) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
apply NNPP.
(* Goal: not (not (@in_part E x A)) *)
(* Goal: not (@in_part E x B) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
red in |- *; intros H'1; try exact H'1.
(* Goal: False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
lapply E0; [ intros H'2; apply H'2; clear E0 | clear E0 ].
(* Goal: and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B) *)
(* Goal: not (@in_part E x B) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
split; [ idtac | intros H'2; try assumption ].
(* Goal: forall _ : @in_part E x B, @in_part E x A *)
(* Goal: forall _ : @in_part E x A, @in_part E x B *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
intros H'2; try assumption.
(* Goal: @cardinal E A n *)
apply H'; auto with *.
(* Goal: @cardinal E A n *)
absurd (in_part x A); auto with *.
(* Goal: not (@Equal E x1 x0) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
red in |- *.
(* Goal: forall _ : @in_part E x B, False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
red in E0.
(* Goal: forall _ : @in_part E x B, False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
intros H'1; try assumption.
(* Goal: False *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
lapply E0; [ intros H'2; apply H'2; clear E0 | clear E0 ].
(* Goal: and (@in_part E x1 A0) (not (@Equal E x1 x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
split; [ try assumption | idtac ].
(* Goal: forall _ : @in_part E x B, @in_part E x A *)
(* Goal: forall _ : @in_part E x A, @in_part E x B *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => not (and (forall _ : @in_part E x B, @in_part E x A) (forall _ : @in_part E x A, @in_part E x B))) *)
intros H'2; try assumption.
(* Goal: @cardinal E A n *)
apply H'; auto with *.
(* Goal: @cardinal E A n *)
auto with *.
apply
 not_all_ex_not
  with
    (P := fun x : E =>
          (in_part x B -> in_part x A) /\ (in_part x A -> in_part x B));
(* Goal: @cardinal E A n *)
 auto with *.
Qed.

Lemma cardinal_included :
 forall (E : Setoid) (A : part_set E) (n : nat),
 cardinal A n ->
 forall B : part_set E,
 included B A -> exists m : nat, cardinal B m /\ m <= n.
(* Goal: forall (E : Setoid) (A : Carrier (part_set E)) (n : nat) (_ : @cardinal E A n) (B : Carrier (part_set E)) (_ : @included E B A), @ex nat (fun m : nat => and (@cardinal E B m) (le m n)) *)
intros E A n H'; try assumption.
apply
 cardinal_ind2
  with
    (P := fun (n : nat) (A : part_set E) (c : cardinal A n) =>
          forall B : part_set E,
          included B A -> ex (fun m : nat => cardinal B m /\ m <= n)).
(* Goal: @cardinal E A n *)
intros A0 H'0 B H'1; exists 0; split; [ try assumption | idtac ]; auto with *.
(* Goal: @cardinal E B O *)
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : @cardinal E B n) (B0 : Carrier (part_set E)) (_ : @included E B0 B), @ex nat (fun m : nat => and (@cardinal E B0 m) (le m n))) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (@add_part E B x)) (_ : @cardinal E A (S n)) (B0 : Carrier (part_set E)) (_ : @included E B0 A), @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n))) *)
(* Goal: @cardinal E A n *)
apply cardinal_empty.
(* Goal: @Equal (part_set E) B (empty E) *)
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : @cardinal E B n) (B0 : Carrier (part_set E)) (_ : @included E B0 B), @ex nat (fun m : nat => and (@cardinal E B0 m) (le m n))) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (@add_part E B x)) (_ : @cardinal E A (S n)) (B0 : Carrier (part_set E)) (_ : @included E B0 A), @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n))) *)
(* Goal: @cardinal E A n *)
inversion H'0.
(* Goal: @cardinal E A n *)
cut (included B (empty E)); auto with *.
(* Goal: @cardinal E A n *)
apply included_comp with B A0; auto with *.
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : @cardinal E B n) (B0 : Carrier (part_set E)) (_ : @included E B0 B), @ex nat (fun m : nat => and (@cardinal E B0 m) (le m n))) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (@add_part E B x)) (_ : @cardinal E A (S n)) (B0 : Carrier (part_set E)) (_ : @included E B0 A), @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n))) *)
(* Goal: @cardinal E A n *)
intros n0 H'0 A0 B x H'1 H'2 H'3 B0 H'4; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
case (classic (Equal B0 A0)); intros.
(* Goal: and True (not (@Equal E y x)) *)
(* Goal: @Equal F x0 (@Ap E F f y) *)
(* Goal: forall _ : not (@Equal E x1 x), @in_part F x0 (@image E F f (@diff E (full E) (@single E x))) *)
(* Goal: lt m (S n0) *)
(* Goal: @cardinal E (@diff E (full E) (@single E x)) n0 *)
exists (S n0); split; [ idtac | try assumption ].
(* Goal: @cardinal E A n *)
apply cardinal_comp with A0 (S n0); auto with *.
(* Goal: @cardinal E A n *)
auto with *.
(* Goal: @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
case (not_included_exist H'4 H).
(* Goal: forall (x : Carrier E) (_ : and (@in_part E x A0) (not (@in_part E x B0))), @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
intros x0 H'5; try assumption.
(* Goal: @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n0))) *)
(* Goal: @cardinal E A n *)
elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
lapply (H'0 (minus_part A0 x0));
 [ intros H'8; elim (H'8 B0);
    [ intros m E0; elim E0; intros H'11 H'12; try exact H'11; clear E0
    | idtac ]
(* Goal: @cardinal E A n *)
 | idtac ]; auto with *.
(* Goal: @ex nat (fun m : nat => and (@cardinal E B0 m) (le m (S n0))) *)
(* Goal: @included E B0 (@minus_part E A0 x0) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
exists m; split; [ try assumption | idtac ].
(* Goal: @cardinal E A n *)
apply le_trans with n0; auto with *.
(* Goal: @in_part E x1 (@diff E A0 (@single E x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
unfold minus_part in |- *; simpl in |- *.
(* Goal: not (@Equal E x1 x0) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
red in |- *.
(* Goal: forall (x : Carrier E) (_ : @in_part E x B0), @in_part E x (@diff E A0 (@single E x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
intros x1 H'5; try assumption.
(* Goal: @in_part E x1 (@diff E A0 (@single E x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
simpl in |- *.
(* Goal: and (@in_part E x1 A0) (not (@Equal E x1 x0)) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
split; [ try assumption | idtac ].
(* Goal: @cardinal E A n *)
apply H'4; auto with *.
(* Goal: not (@Equal E x1 x0) *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
red in |- *.
(* Goal: forall _ : @Equal E x1 x0, False *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
intros H'9; try assumption.
(* Goal: False *)
(* Goal: @cardinal E (@minus_part E A0 x0) n0 *)
(* Goal: @cardinal E A n *)
apply H'7.
(* Goal: @cardinal E A n *)
apply in_part_comp_l with x1; auto with *.
(* Goal: @cardinal E A n *)
apply cardinal_S with A0 x0; auto with *.
(* Goal: @Equal (part_set E) A0 (@add_part E (@minus_part E A0 x0) x0) *)
(* Goal: @cardinal E A n *)
apply Sym.
(* Goal: @cardinal E A n *)
apply minus_add; auto with *.
(* Goal: @cardinal E A n *)
auto with *.
Qed.

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.
(* Goal: not (@eq nat x n) *)
(* Goal: @eq nat x n *)
intros A B f n m H' H'0 H'1; red in |- *; intros H'2; try exact H'2.
(* Goal: False *)
red in H'2.
(* Goal: @cardinal E A n *)
case (tiroirs (E:=A) (F:=B) (f:=f) H' H'0 H'1); auto with *.
(* Goal: forall (x : Carrier A) (_ : @ex (Carrier A) (fun y : Carrier A => and (not (@Equal A x y)) (@Equal B (@Ap A B f x) (@Ap A B f y)))), False *)
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;
(* Goal: @cardinal E A n *)
 auto with *.
Qed.

Definition finite (A : Setoid) := exists n : nat, cardinal (full A) n.