diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 33d351edcb7bb2c953120661c0b7a1afeabb0a9b..0c328a779a1d2cf59d51c9b9e2d9726eba91d17c 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -39,12 +39,6 @@ Arguments Affine {_} _%I : simpl never.
 Arguments affine {_} _%I {_}.
 Hint Mode Affine + ! : typeclass_instances.
 
-Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
-Existing Instance absorbing_bi | 0.
-
-Class BiPositive (PROP : bi) :=
-  bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
-
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_absorbingly {_} _%I : simpl never.
 Instance: Params (@bi_absorbingly) 1.
@@ -703,6 +697,10 @@ Global Instance affinely_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely PROP).
 Proof. solve_proper. Qed.
 
+Lemma bi_positive_affinely `{BiPositive PROP} (P Q : PROP) :
+  bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
+Proof. apply bi_positive. Qed.
+
 Lemma affinely_elim_emp P : bi_affinely P ⊢ emp.
 Proof. rewrite /bi_affinely; auto. Qed.
 Lemma affinely_elim P : bi_affinely P ⊢ P.
@@ -736,7 +734,8 @@ Lemma affinely_sep `{BiPositive PROP} P Q :
   bi_affinely (P ∗ Q) ⊣⊢ bi_affinely P ∗ bi_affinely Q.
 Proof.
   apply (anti_symm _), affinely_sep_2.
-  by rewrite -{1}affinely_idemp bi_positive !(comm _ (bi_affinely P)%I) bi_positive.
+  by rewrite -{1}affinely_idemp bi_positive_affinely
+                 !(comm _ (bi_affinely P)%I) bi_positive_affinely.
 Qed.
 Lemma affinely_forall {A} (Φ : A → PROP) :
   bi_affinely (∀ a, Φ a) ⊢ ∀ a, bi_affinely (Φ a).
@@ -878,10 +877,12 @@ Proof. by rewrite comm True_sep. Qed.
 Section bi_affine.
   Context `{BiAffine PROP}.
 
+  Global Instance bi_affine_affine P : Affine P | 0.
+  Proof. apply bi_affine. Qed.
   Global Instance bi_affine_absorbing P : Absorbing P | 0.
   Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
   Global Instance bi_affine_positive : BiPositive PROP.
-  Proof. intros P Q. by rewrite !affine_affinely. Qed.
+  Proof. intros P Q. by rewrite !emp_and. Qed.
 
   Lemma True_emp : True ⊣⊢ emp.
   Proof. apply (anti_symm _); auto using affine. Qed.
@@ -1085,7 +1086,7 @@ Section persistently_affinely_bi.
     bi_persistently P ∧ Q ⊣⊢ bi_persistently P ∗ Q.
   Proof.
     apply (anti_symm (⊢));
-      eauto using persistently_and_sep_l_1, sep_and with typeclass_instances.
+      eauto 10 using persistently_and_sep_l_1, sep_and with typeclass_instances.
   Qed.
   Lemma persistently_and_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ bi_persistently Q.
   Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
@@ -1279,7 +1280,7 @@ Section plainly_affinely_bi.
   Lemma plainly_and_sep_l P Q : bi_plainly P ∧ Q ⊣⊢ bi_plainly P ∗ Q.
   Proof.
     apply (anti_symm (⊢));
-      eauto using plainly_and_sep_l_1, sep_and with typeclass_instances.
+      eauto 10 using plainly_and_sep_l_1, sep_and with typeclass_instances.
   Qed.
   Lemma plainly_and_sep_r P Q : P ∧ bi_plainly Q ⊣⊢ P ∗ bi_plainly Q.
   Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed.
@@ -1521,11 +1522,14 @@ Proof. by intros ->. Qed.
 
 Lemma plainly_if_pure p φ : bi_plainly_if p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. destruct p; simpl; auto using plainly_pure. Qed.
-Lemma plainly_if_and p P Q : bi_plainly_if p (P ∧ Q) ⊣⊢ bi_plainly_if p P ∧ bi_plainly_if p Q.
+Lemma plainly_if_and p P Q :
+  bi_plainly_if p (P ∧ Q) ⊣⊢ bi_plainly_if p P ∧ bi_plainly_if p Q.
 Proof. destruct p; simpl; auto using plainly_and. Qed.
-Lemma plainly_if_or p P Q : bi_plainly_if p (P ∨ Q) ⊣⊢ bi_plainly_if p P ∨ bi_plainly_if p Q.
+Lemma plainly_if_or p P Q :
+  bi_plainly_if p (P ∨ Q) ⊣⊢ bi_plainly_if p P ∨ bi_plainly_if p Q.
 Proof. destruct p; simpl; auto using plainly_or. Qed.
-Lemma plainly_if_exist {A} p (Ψ : A → PROP) : (bi_plainly_if p (∃ a, Ψ a)) ⊣⊢ ∃ a, bi_plainly_if p (Ψ a).
+Lemma plainly_if_exist {A} p (Ψ : A → PROP) :
+  (bi_plainly_if p (∃ a, Ψ a)) ⊣⊢ ∃ a, bi_plainly_if p (Ψ a).
 Proof. destruct p; simpl; auto using plainly_exist. Qed.
 Lemma plainly_if_sep `{BiPositive PROP} p P Q :
   bi_plainly_if p (P ∗ Q) ⊣⊢ bi_plainly_if p P ∗ bi_plainly_if p Q.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 70ccc5f42572c76e6a8254e8187e0474d8054f37..549082bc9321ee90b923b3d4d80a4687b3a34d64 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -331,6 +331,11 @@ Coercion sbi_valid {PROP : sbi} : PROP → Prop := bi_valid.
 Arguments bi_valid {_} _%I : simpl never.
 Typeclasses Opaque bi_valid.
 
+Class BiAffine (PROP : bi) := bi_affine (Q : PROP) : Q ⊢ emp.
+
+Class BiPositive (PROP : bi) :=
+  bi_positive (P Q : PROP) : emp ∧ (P ∗ Q) ⊢ (emp ∧ P) ∗ Q.
+
 Module bi.
 Section bi_laws.
 Context {PROP : bi}.