proposition: Lemma Endo_Injective_Surjective : forall A, Finite A -> decidable_eq A -> forall f:A->A, Injective f <-> Surjective f.
proof: Proof. intros A F d f. rewrite (Surjective_carac F d). split. - assert (Finite' A) as (l, L) by (now apply Finite_dec); clear F. rewrite (Injective_carac L); intros. exists l; split; trivial. destruct L as (N,F). assert (I : incl l (map f l)). { apply NoDup_length_incl; trivial. - now rewrite map_length. - intros x _. apply F. } intros x. apply I, F. - clear F d. intros (l,L). assert (N : NoDup l). { apply (NoDup_map_inv f), L. } assert (I : incl (map f l) l). { apply NoDup_length_incl; trivial. - now rewrite map_length. - intros x _. apply L. } assert (L' : Listing l). { split; trivial. intro x. apply I, L. } apply (Injective_carac L'), L. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec