Stronger local update for multisets that entails the old ones.

theories/algebra/gmultiset.v

@@ -61,19 +61,22 @@ Section gmultiset.
   Lemma gmultiset_update X Y : X ~~> Y.
   Proof. done. Qed.
 
-  Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X ⊎ X', Y ⊎ X').
+  Lemma gmultiset_local_update X Y X' Y' : X ⊎ Y' = X' ⊎ Y → (X,Y) ~l~> (X', Y').
   Proof.
-    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split. done. rewrite !gmultiset_op_disj_union.
-    by rewrite -!assoc (comm _ Z' X').
+    intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
+    split; first done. apply leibniz_equiv_iff, (inj (⊎ Y)).
+    rewrite -HXY !gmultiset_op_disj_union.
+    by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
   Qed.
 
+  Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X ⊎ X', Y ⊎ X').
+  Proof. apply gmultiset_local_update. by rewrite (comm_L _ Y) assoc_L. Qed.
+
   Lemma gmultiset_local_update_dealloc X Y X' :
     X' ⊆ X → X' ⊆ Y → (X,Y) ~l~> (X ∖ X', Y ∖ X').
   Proof.
     intros ->%gmultiset_disj_union_difference ->%gmultiset_disj_union_difference.
-    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split. done. rewrite !gmultiset_op_disj_union=> x.
+    apply gmultiset_local_update. apply gmultiset_eq=> x.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
     lia.
   Qed.