surjective_finite

Prove that Finite B knowing that Finite A and there exists a surjection f from A to B.

theories/finite.v

@@ -220,15 +220,26 @@ Section enc_finite.
   Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
 End enc_finite.
 
+Section surjective_finite.
+  Context `{Finite A, EqDecision B} (f : A → B).
+  Context `{!Surj (=) f}.
+
+  Program Instance surjective_finite: Finite B :=
+    {| enum := remove_dups (f <$> enum A) |}.
+  Next Obligation. apply NoDup_remove_dups. Qed.
+  Next Obligation.
+    intros y. rewrite elem_of_remove_dups, elem_of_list_fmap.
+    destruct (surj f y). eauto using elem_of_enum.
+  Qed.
+End surjective_finite.
+
 Section bijective_finite.
   Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
   Context `{!Inj (=) (=) f, !Cancel (=) f g}.
 
-  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
-  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
-  Next Obligation.
-    intros y. rewrite elem_of_list_fmap. eauto using elem_of_enum.
-  Qed.
+  Global Instance bijective_finite: Finite B :=
+    let _ := cancel_surj (f:=f) (g:=g) in
+    surjective_finite f.
 End bijective_finite.
 
 Program Instance option_finite `{Finite A} : Finite (option A) :=