proposition: Lemma Surjective_inverse : forall A B, Finite A -> EqDec B -> forall f:A->B, Surjective f -> exists g:B->A, forall x, f (g x) = x.
proof: Proof. intros A B F d f Su. destruct (Finite_Empty_or_not F) as [noA | (a,_)]. - assert (noB : B -> False). { intros y. now destruct (Su y). } exists (fun y => False_rect _ (noB y)). intro y. destruct (noB y). - destruct F as (l,F). set (h := fun x k => if d (f k) x then true else false). set (get := fun o => match o with Some y => y | None => a end). exists (fun x => get (List.find (h x) l)). intros x. case_eq (find (h x) l); simpl; clear get; [intros y H|intros H]. * apply find_some in H. destruct H as (_,H). unfold h in H. now destruct (d (f y) x) in H. * exfalso. destruct (Su x) as (y & Y). generalize (find_none _ l H y (F y)). unfold h. now destruct (d (f y) x). Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec