diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index d73745c2c2e808effd1d42b78a1af71313474776..71c86a043d5874a7bd7d4e71962d43b1fbfec49b 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -169,11 +169,15 @@ Section ofe.
   Proof. induction 2; eauto using dist_S. Qed.
   Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
   Proof. intros; eauto using dist_le. Qed.
-  Instance ne_proper {B : ofeT} (f : A → B) `{!NonExpansive f} :
-    Proper ((≡) ==> (≡)) f | 100.
+  (** [ne_proper] and [ne_proper_2] are not instances to improve efficiency of
+  type class search during setoid rewriting.
+  Instances of [NonExpansive{,2}] are hence accompanied by instances of
+  [Proper] built using these lemmas. *)
+  Lemma ne_proper {B : ofeT} (f : A → B) `{!NonExpansive f} :
+    Proper ((≡) ==> (≡)) f.
   Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
-  Instance ne_proper_2 {B C : ofeT} (f : A → B → C) `{!NonExpansive2 f} :
-    Proper ((≡) ==> (≡) ==> (≡)) f | 100.
+  Lemma ne_proper_2 {B C : ofeT} (f : A → B → C) `{!NonExpansive2 f} :
+    Proper ((≡) ==> (≡) ==> (≡)) f.
   Proof.
      unfold Proper, respectful; setoid_rewrite equiv_dist.
      by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).