proposition: Lemma Injective_Surjective_Bijective : forall A B, Finite A -> EqDec B -> forall f:A->B, Injective f -> Surjective f -> Bijective f.
proof: Proof. intros A B F d f Ij Su. destruct (Surjective_inverse F d Su) as (g, E). exists g. split; trivial. intros y. apply Ij. now rewrite E. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec