proposition: 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.
proof: Proof. intros E F f n H' H'0 H'1; try assumption. apply cardinal_image_equal_injective with n; auto with *. apply cardinal_comp with (full F) n; auto with *. apply Sym; auto with *. Qed.
imports: Tiroirs Parts2 Classical_Pred_Type Compare_dec