proposition: Lemma map_disjoint_filter_complement {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) : filter P m ##ₘ filter (λ v, ¬ P v) m.
proof: Proof. apply map_disjoint_spec. intros i x y. rewrite !map_lookup_filter_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)