[B] Move FiniteTypes.finite_couple to Finite_sets

This ensures that `FiniteTypes.v` contains only lemmas & theorems
concerning `FiniteT`.
Use `Finite_sets.finite_couple` instead now.

theories/ZornsLemma/CountableTypes.v

@@ -2,7 +2,7 @@ From Coq Require Export Relation_Definitions QArith ZArith.
 From Coq Require Import Arith ArithRing FunctionalExtensionality
     Program.Subset ClassicalChoice.
 From ZornsLemma Require Import InfiniteTypes CSB DecidableDec
-    DependentTypeChoice.
+    DependentTypeChoice Finite_sets.
 From ZornsLemma Require Export FiniteTypes IndexedFamilies.
 
 Local Close Scope Q_scope.

theories/ZornsLemma/FiniteTypes.v

@@ -979,11 +979,3 @@ Proof.
     + intros. destruct x as [[]|]; intuition.
     + intros. destruct y as [|]; intuition.
 Qed.
-
-Lemma finite_couple {X} (x y : X) :
-  Finite (Couple x y).
-Proof.
-  rewrite <- Couple_as_union.
-  apply Union_preserves_Finite.
-  all: apply Singleton_is_finite.
-Qed.

theories/ZornsLemma/Finite_sets.v

@@ -1,6 +1,14 @@
 From Coq Require Import Classical.
-From Coq Require Export Finite_sets.
-From ZornsLemma Require Import EnsemblesImplicit FiniteImplicit.
+From Coq Require Export Finite_sets Finite_sets_facts.
+From ZornsLemma Require Import EnsemblesImplicit FiniteImplicit Powerset_facts.
+
+Lemma finite_couple {X} (x y : X) :
+  Finite (Couple x y).
+Proof.
+  rewrite <- Couple_as_union.
+  apply Union_preserves_Finite.
+  all: apply Singleton_is_finite.
+Qed.
 
 (* This is like a choice property for finite sets. And [P] is about pairs, so
    that's the meaning of the name. It is similar to