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. } 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). subst. rewrite ?H1 in H3. subst. reflexivity. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)