diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 542b42df8e3c915360ac05b715ae59449ce2f0ec..d5b23357d1db1dd6fc563c222d0b55b8078293ff 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -797,6 +797,20 @@ Section proto.
       iNext. by iRewrite "Hp2d".
   Qed.
 
+  Lemma iProto_le_dual_l p1 p2 :
+    iProto_le (iProto_dual p2) p1 -∗ iProto_le (iProto_dual p1) p2.
+  Proof.
+    iIntros "H". iEval (rewrite -(iProto_dual_involutive p2)).
+    by iApply iProto_le_dual.
+  Qed.
+
+  Lemma iProto_le_dual_r p1 p2 :
+    iProto_le p2 (iProto_dual p1) -∗ iProto_le p1 (iProto_dual p2).
+  Proof.
+    iIntros "H". iEval (rewrite -(iProto_dual_involutive p1)).
+    by iApply iProto_le_dual.
+  Qed.
+
   Lemma iProto_le_app p1 p2 p3 p4 :
     iProto_le p1 p2 -∗ iProto_le p3 p4 -∗ iProto_le (p1 <++> p3) (p2 <++> p4).
   Proof.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index ab5f6f556840ae0dd812b5d8781a3a661d0a8f05..54f5b6554e564c5740483ecb2719f552c20927c0 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -295,6 +295,12 @@ Section subtype.
   Lemma lsty_le_dual S1 S2 : S2 <s: S1 -∗ lsty_dual S1 <s: lsty_dual S2.
   Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
 
+  Lemma lsty_le_dual_l S1 S2 : lsty_dual S2 <s: S1 -∗ lsty_dual S1 <s: S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_l. Qed.
+
+  Lemma lsty_le_dual_r S1 S2 : S2 <s: lsty_dual S1 -∗ S1 <s: lsty_dual S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.
+
   Lemma lsty_le_rec_1 (C : lsty Σ → lsty Σ) `{!Contractive C} :
     ⊢ lsty_rec C <s: C (lsty_rec C).
   Proof.