diff --git a/modures/ra.v b/modures/ra.v
index a3c5d4e0ba4531476a875a9526bc743fc66fe859..8525136bb51506454cc98e832f793935f13ae87b 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -125,6 +125,10 @@ Lemma ra_empty_least x : ∅ ≼ x.
 Proof. by exists x; rewrite (left_id _ _). Qed.
 
 (** * Big ops *)
+Lemma big_op_nil : big_op (@nil A) = ∅.
+Proof. done. Qed.
+Lemma big_op_cons x xs : big_op (x :: xs) = x â‹… big_op xs.
+Proof. done. Qed.
 Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
 Proof.
   induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
@@ -147,6 +151,9 @@ Proof.
   * by transitivity (big_op ys); [|apply ra_included_r].
   * by transitivity (big_op ys).
 Qed.
+Lemma big_op_delete xs i x :
+  xs !! i = Some x → x ⋅ big_op (delete i xs) ≡ big_op xs.
+Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.
 
 Context `{FinMap K M}.
 Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.