diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b6..4d691af761 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `cardinality.v`:
+  + lemma `infinite_setD`
+
 ### Changed
 
 ### Renamed
diff --git a/classical/cardinality.v b/classical/cardinality.v
index cd220934ad..62bfb08099 100644
--- a/classical/cardinality.v
+++ b/classical/cardinality.v
@@ -1002,6 +1002,14 @@ move=> /finite_setP[m Am]; rewrite (card_fset_set Am).
 by rewrite (card_le_eqr Am) card_le_II.
 Qed.
 
+Lemma infinite_setD {T} (A B : set T) :
+  infinite_set A -> finite_set B -> infinite_set (A `\` B).
+Proof.
+move=> + finB finAB; apply.
+have : finite_set ((A `&` ~` B) `|` B) by rewrite finite_setU.
+by rewrite setUIl setUCl setIT finite_setU => -[].
+Qed.
+
 Lemma infinite_set_fset {T : choiceType} (A : set T) n :
   infinite_set A ->
     exists2 B : {fset T}, [set` B] `<=` A & (#|` B| >= n)%N.