Make filter lemmas for maps and sets consistent + add cross split property for maps

We have the following lemmas for the combination of filter and union/disjoint for maps and sets:

Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
  filter P m ∪ filter (λ v, ¬ P v) m = m.
Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
  filter P m ##ₘ filter (λ v, ¬ P v) m.

Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.

There are two things that are strange here:

• The naming scheme is inconsistent: union_filter vs filter_union
• The statements of the union+filter lemmas is inconsistent

This MR aims to make the set of lemmas for maps and sets consistent. Concretely:

• Sets: Add lemmas disjoint_filter, disjoint_filter_complement, and filter_union_complement.
• Maps: Rename map_disjoint_filter → map_disjoint_filter_complement and map_union_filter → map_filter_union_complement to be consistent with sets.
• Maps: Add lemmas map_disjoint_filter and map_filter_union analogous to sets.
• Maps: Use filter lemmas to prove cross split property.