proposition: Lemma coPset_split_infinite (X : coPset) : set_infinite X → ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ set_infinite X1 ∧ set_infinite X2.
proof: Proof. setoid_rewrite coPset_infinite_finite. eapply coPset_split. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)