diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 27fc8f8d4e1cf29c17997ec7f2ada3716edc99f0..1323605d1c0f855b8a6f6942d9c9fcfa4693f434 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -555,11 +555,15 @@ Proof.
   split; first by rewrite cmra_valid_validN.
   eauto using cmra_discrete_valid, cmra_validN_le with lia.
 Qed.
+Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete A} n x : ✓{0} x ↔ ✓{n} x.
+Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
 Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
 Proof.
   split; first by apply cmra_included_includedN.
   intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
 Qed.
+Lemma cmra_discrete_included_iff_0 `{OfeDiscrete A} n x y : x ≼{0} y ↔ x ≼{n} y.
+Proof. by rewrite -!cmra_discrete_included_iff. Qed.
 
 (** Cancelable elements  *)
 Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index eb422ac9b8a73bb933c48f2cfa10cd34bd47bc6a..12686722d65d534c745a5ce84296d8424088a404 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -190,9 +190,7 @@ Section ofe.
     split; intros; auto. apply (discrete _), dist_le with n; auto with lia.
   Qed.
   Lemma discrete_iff_0 n (x : A) `{!Discrete x} y : x ≡{0}≡ y ↔ x ≡{n}≡ y.
-  Proof.
-    split=> ?. by apply equiv_dist, (discrete _). eauto using dist_le with lia.
-  Qed.
+  Proof. by rewrite -!discrete_iff. Qed.
 End ofe.
 
 (** Contractive functions *)