diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index adf77d0fabdfacde5470cd33df01b7e55f9c7778..4b2a013f6fc5abb7c2842f6335699543fa2862c7 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -127,7 +127,7 @@ Section dfrac.
     intros [q| |q];
       rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid /=.
     - apply (Qp_not_plus_ge 1 q).
-    - move=>/Qclt_not_eq. intros Heq. apply Heq. done.
+    - intros []%irreflexivity. apply _.
     - move=> /Qclt_le_weak. apply (Qp_not_plus_ge 1 q).
   Qed.