Redundant preconditions for map_disjoint_difference_l and map_disjoint_difference_r

Hi, the preconditions for map_disjoint_difference_l and map_disjoint_difference_r can be removed. I cannot create a PR so here is my local diff instead:

> git diff
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 87f1f2c..d119e7e 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -3041,14 +3041,13 @@ Proof.
   rewrite lookup_difference.
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
-Lemma map_disjoint_difference_l {A} (m1 m2 : M A) : m1 ⊆ m2 → m2 ∖ m1 ##ₘ m1.
+Lemma map_disjoint_difference_l {A} (m1 m2 : M A) : m2 ∖ m1 ##ₘ m1.
 Proof.
-  intros Hm i; specialize (Hm i).
-  unfold difference, map_difference; rewrite lookup_difference_with.
+  intro i. unfold difference, map_difference; rewrite lookup_difference_with.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
-Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ##ₘ m2 ∖ m1.
-Proof. intros. symmetry. by apply map_disjoint_difference_l. Qed.
+Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : m1 ##ₘ m2 ∖ m1.
+Proof. symmetry. by apply map_disjoint_difference_l. Qed.
 Lemma map_subseteq_difference_l {A} (m1 m2 m : M A) : m1 ⊆ m → m1 ∖ m2 ⊆ m.
 Proof.
   rewrite !map_subseteq_spec. setoid_rewrite lookup_difference_Some. naive_solver.

If easier, can create a PR instead if given access.