Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None

theories/fin_map_dom.v

@@ -42,6 +42,10 @@ Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom m.
 Proof. rewrite elem_of_dom; eauto. Qed.
 Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom m ↔ m !! i = None.
 Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
+Lemma not_elem_of_dom_1 {A} (m : M A) i : i ∉ dom m → m !! i = None.
+Proof. apply not_elem_of_dom. Qed.
+Lemma not_elem_of_dom_2 {A} (m : M A) i : m !! i = None → i ∉ dom m.
+Proof. apply not_elem_of_dom. Qed.
 Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom m1 ⊆ dom m2.
 Proof.
   rewrite map_subseteq_spec.

theories/fin_maps.v

@@ -2273,6 +2273,12 @@ Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 Lemma lookup_union_None {A} (m1 m2 : M A) i :
   (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
 Proof. rewrite lookup_union.  destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
+Lemma lookup_union_None_1 {A} (m1 m2 : M A) i :
+  (m1 ∪ m2) !! i = None → m1 !! i = None ∧ m2 !! i = None.
+Proof. apply lookup_union_None. Qed.
+Lemma lookup_union_None_2 {A} (m1 m2 : M A) i :
+  m1 !! i = None → m2 !! i = None → (m1 ∪ m2) !! i = None.
+Proof. intros. by apply lookup_union_None. Qed.
 Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
   m1 ##ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
 Proof.