proposition: Lemma finite_couple {X} (x y : X) : Finite (Couple x y).
proof: Proof. rewrite <- Couple_as_union. apply Union_preserves_Finite. all: apply Singleton_is_finite. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)