proposition: 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.
proof: Proof. intros E F f n H' H'0 H'1; try assumption. generalize (cardinal_image_injective H' H'1). intros H'2; try assumption. apply image_full_surjective; auto with *. unfold image_map in |- *. apply cardinal_equal_included_equal with n; auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec