diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index d1401ef1136a7c23d044583c7d3b86f63acb1013..96f1a3d6dec1b2edc7191f701444afbaada3c65d 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -48,5 +48,8 @@ Proof.
   eapply Qclt_not_eq; first done. by apply (inj (Qcplus q)).
 Qed.
 
-Lemma frac_op': ∀ (p q: Qp), (p ⋅ q) = (p + q)%Qp.
+Lemma frac_op' (q p : Qp) : (p â‹… q) = (p + q)%Qp.
+Proof. done. Qed.
+
+Lemma frac_valid' (p : Qp) : ✓ p ↔ (p ≤ 1%Qp)%Qc.
 Proof. done. Qed.