proposition: Lemma coPset_split (X : coPset) : ¬set_finite X → ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ ¬set_finite X1 ∧ ¬set_finite X2.
proof: Proof. exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union, coPset_lr_disjoint, coPset_l_finite, coPset_r_finite. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)