From ad0c229de9baa848af05bfc10f7d8c02c9100efb Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Mon, 10 Oct 2016 14:23:20 +0200
Subject: [PATCH] Add rewrite lemma for frac_op

---
 algebra/frac.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/algebra/frac.v b/algebra/frac.v
index 11cb32dea..bc9f469df 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -35,3 +35,6 @@ Global Instance frac_full_exclusive : Exclusive 1%Qp.
 Proof.
   move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
 Qed.
+
+Lemma frac_op': ∀ (p q: Qp), (p ⋅ q) = (p + q)%Qp.
+Proof. done. Qed.
-- 
GitLab