diff --git a/theories/coPset.v b/theories/coPset.v
index e86d831d6ee7cf8cb3ea09171c1a7b95ffe47c93..8e8cb978c846d563b3c6c2042efe6805cecea937 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -453,3 +453,10 @@ Proof.
   exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union,
     coPset_lr_disjoint, coPset_l_finite, coPset_r_finite.
 Qed.
+Lemma coPset_split_infinite (X : coPset) :
+  set_infinite X →
+  ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ set_infinite X1 ∧ set_infinite X2.
+Proof.
+  setoid_rewrite coPset_infinite_finite.
+  eapply coPset_split.
+Qed.