From b8dc077371ac9fbe45bb3f8ffe267ffac19e139a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Mar 2017 16:29:40 +0100
Subject: [PATCH] make frac_included into general lemma about < and + of
 positive fractions

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

diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 96f1a3d6d..7dfd5b92e 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -11,14 +11,19 @@ Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
 Instance frac_pcore : PCore frac := λ _, None.
 Instance frac_op : Op frac := λ x y, (x + y)%Qp.
 
-Lemma frac_included (x y : frac) : x ≼ y ↔ (x < y)%Qc.
+(* TODO: Find better place for this lemma. *)
+Lemma Qp_le_sum (x y : Qp) : (x < y)%Qc ↔ (∃ z, y = x + z)%Qp.
 Proof.
   split.
-  - intros [z ->%leibniz_equiv]; simpl.
-    rewrite -{1}(Qcplus_0_r x). apply Qcplus_lt_mono_l, Qp_prf.
   - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl.
     by rewrite (Qcplus_comm y) Qcplus_assoc Qcplus_opp_r Qcplus_0_l.
+  - intros [z ->%leibniz_equiv]; simpl.
+    rewrite -{1}(Qcplus_0_r x). apply Qcplus_lt_mono_l, Qp_prf.
 Qed.
+
+Lemma frac_included (x y : frac) : x ≼ y ↔ (x < y)%Qc.
+Proof. symmetry. exact: Qp_le_sum. Qed.
+
 Corollary frac_included_weak (x y : frac) : x ≼ y → (x ≤ y)%Qc.
 Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
 
-- 
GitLab