proposition: Lemma Surjective_carac A B : Finite B -> decidable_eq B -> forall f:A->B, Surjective f <-> (exists lA, Listing (map f lA)).
proof: Proof. intros (lB,FB) d f. split. - rewrite Surjective_list_carac. intros Su. destruct (Su lB) as (lA,IC). destruct (uniquify_map d f lA) as (lA' & N & IC'). exists lA'. split; trivial. intro x. apply IC', IC, FB. - intros (lA & N & FA) y. generalize (FA y). rewrite in_map_iff. intros (x & E & _). now exists x. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec