diff --git a/algebra/upred.v b/algebra/upred.v
index d0a4d6f676be333bf5462c2a6c6c4d002d66da73..848ba2ad56dd2605b2c54918fba4ed37cf2484e2 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -576,6 +576,10 @@ Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
 
 (* Derived BI Stuff *)
 Hint Resolve sep_mono.
+Lemma sep_mono_l P P' Q : P ⊑ Q → (P ★ P') ⊑ (Q ★ P').
+Proof. by intros; apply sep_mono. Qed.
+Lemma sep_mono_r P P' Q' : P' ⊑ Q' → (P ★ P') ⊑ (P ★ Q').
+Proof. by apply sep_mono. Qed.
 Global Instance sep_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_sep M).
 Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
 Global Instance sep_flip_mono' :