proposition: Lemma coPset_infinite_finite (X : coPset) : set_infinite X ↔ ¬set_finite X.
proof: Proof. split; [intros ??; by apply (set_not_infinite_finite X)|]. intros Hfin xs. exists (coPpick (X ∖ list_to_set xs)). cut (coPpick (X ∖ list_to_set xs) ∈ X ∖ list_to_set xs); [set_solver|]. apply coPpick_elem_of; intros Hfin'. apply Hfin, (difference_finite_inv _ (list_to_set xs)), Hfin'. apply list_to_set_finite. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)