From a8f65af5185fe60be2af279e39e5fe28d4fda2f1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 May 2018 18:59:49 +0200
Subject: [PATCH] Misc results about `Qp` fractions.

---
 theories/numbers.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/numbers.v b/theories/numbers.v
index 1eb8e1fc..28227372 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -608,6 +608,12 @@ Lemma Qp_div_2 x : (x / 2 + x / 2 = x)%Qp.
 Proof.
   change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1.
 Qed.
+Lemma Qp_half_half : (1 / 2 + 1 / 2 = 1)%Qp.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma Qp_quarter_three_quarter : (1 / 4 + 3 / 4 = 1)%Qp.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma Qp_three_quarter_quarter : (3 / 4 + 1 / 4 = 1)%Qp.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
 
 Lemma Qp_lt_sum (x y : Qp) : (x < y)%Qc ↔ ∃ z, y = (x + z)%Qp.
 Proof.
-- 
GitLab