diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index fac8024f36dc37e7aab994ee9a37ed7ec0b9d900..f0a8571482343154899b2385de7c379f3dd8ee83 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -743,7 +743,7 @@ Lemma sep_elim_r P Q `{TCOr (Affine P) (Absorbing Q)} : P ∗ Q ⊢ Q.
 Proof. by rewrite comm sep_elim_l. Qed.
 
 Lemma sep_and P Q :
-  TCOr (Affine P) (Absorbing Q) → TCOr (Absorbing P) (Affine Q) →
+  TCOr (Affine P) (Absorbing Q) → TCOr (Affine Q) (Absorbing P) →
   P ∗ Q ⊢ P ∧ Q.
 Proof.
   intros [?|?] [?|?];
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 7415815167b4558c1c9984dc490b68516b1476b8..765cd82abfa9c080cb0536ac705e92e16feeaeed 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -640,7 +640,7 @@ Proof. intros. by rewrite /FromAnd big_sepMS_disj_union persistent_and_sep_1. Qe
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
 Proof. by rewrite /FromSep. Qed.
 Global Instance from_sep_and P1 P2 :
-  TCOr (Affine P1) (Absorbing P2) → TCOr (Absorbing P1) (Affine P2) →
+  TCOr (Affine P1) (Absorbing P2) → TCOr (Affine P2) (Absorbing P1) →
   FromSep (P1 ∧ P2) P1 P2 | 101.
 Proof. intros. by rewrite /FromSep sep_and. Qed.
 
@@ -758,7 +758,7 @@ Proof.
     -and_sep_intuitionistically intuitionistically_and //.
 Qed.
 Global Instance into_and_sep_affine p P Q :
-  TCOr (Affine P) (Absorbing Q) → TCOr (Absorbing P) (Affine Q) →
+  TCOr (Affine P) (Absorbing Q) → TCOr (Affine Q) (Absorbing P) →
   IntoAnd p (P ∗ Q) P Q.
 Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
 
@@ -838,7 +838,7 @@ Global Instance into_sep_persistently `{!BiPositive PROP} P Q1 Q2 :
 Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
 Global Instance into_sep_persistently_affine P Q1 Q2 :
   IntoSep P Q1 Q2 →
-  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) →
+  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
   IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof.
   rewrite /IntoSep /= => -> ??.
@@ -846,7 +846,7 @@ Proof.
 Qed.
 Global Instance into_sep_intuitionistically_affine P Q1 Q2 :
   IntoSep P Q1 Q2 →
-  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) →
+  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
   IntoSep (â–¡ P) (â–¡ Q1) (â–¡ Q2).
 Proof.
   rewrite /IntoSep /= => -> ??.
diff --git a/iris/proofmode/class_instances_plainly.v b/iris/proofmode/class_instances_plainly.v
index c87e3ff53ab1b113107dc261a56fcd0203a93c2e..0971f80cd2681716ba5cd883c0631061efb0010f 100644
--- a/iris/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -57,7 +57,7 @@ Global Instance into_sep_plainly `{!BiPositive PROP} P Q1 Q2 :
 Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
 Global Instance into_sep_plainly_affine P Q1 Q2 :
   IntoSep P Q1 Q2 →
-  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) →
+  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
   IntoSep (â–  P) (â–  Q1) (â–  Q2).
 Proof.
   rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.