From 5874f41e10c229d0b7df07a1e4e58f5e61a1af0a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Mar 2017 17:32:37 +0100
Subject: [PATCH] show frac_valid'

---
 theories/algebra/frac.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index d1401ef11..96f1a3d6d 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.
-- 
GitLab