proposition: Lemma coPset_elem_of_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t).
proof: Proof. by revert p; induction t as [[]|[]]; intros [?|?|]; simpl; rewrite ?coPset_elem_of_node; simpl. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)