proposition: Lemma finite_surj_inj: forall (X:Type) (f:X->X), FiniteT X -> surjective f -> injective f.
proof: Proof. intros. assert (exists g:X->X, forall x:X, f (g x) = x). apply finite_choice with (R:=fun (x y:X) => f y = x). assumption. assumption. destruct H1 as [g]. assert (surjective g). apply finite_inj_surj. assumption. red; intros. rewrite <- H1 with x. rewrite <- H1 with y. rewrite H2; reflexivity. red; intros. destruct (H2 x). destruct (H2 y). rewrite <- H4 in H3. rewrite <- H5 in H3. repeat rewrite H1 in H3. rewrite <- H4. rewrite <- H5. rewrite H3. reflexivity. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description