From a60c821e53b5391d59efc97666efeedaf0bd1c9c Mon Sep 17 00:00:00 2001
From: Columbus240 <8899730+Columbus240@users.noreply.github.com>
Date: Fri, 17 Jun 2022 09:44:07 +0200
Subject: [PATCH] [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 +-
 theories/ZornsLemma/FiniteTypes.v    |  8 --------
 theories/ZornsLemma/Finite_sets.v    | 12 ++++++++++--
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/theories/ZornsLemma/CountableTypes.v b/theories/ZornsLemma/CountableTypes.v
index 3a432639..9dc1ca55 100644
--- a/theories/ZornsLemma/CountableTypes.v
+++ b/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.
diff --git a/theories/ZornsLemma/FiniteTypes.v b/theories/ZornsLemma/FiniteTypes.v
index fff37951..8779d224 100644
--- a/theories/ZornsLemma/FiniteTypes.v
+++ b/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.
diff --git a/theories/ZornsLemma/Finite_sets.v b/theories/ZornsLemma/Finite_sets.v
index f04fe76e..88b27415 100644
--- a/theories/ZornsLemma/Finite_sets.v
+++ b/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