From e29a5aeee28cde833b37cc869eec7c73970be120 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 May 2018 18:59:31 +0200
Subject: [PATCH] Literals 2, 3, and 4 for `Qp`.

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

diff --git a/theories/numbers.v b/theories/numbers.v
index 4be6c114..1eb8e1fc 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -541,11 +541,14 @@ Next Obligation.
     <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
 Qed.
 
-Notation "1" := Qp_one : Qp_scope.
 Infix "+" := Qp_plus : Qp_scope.
 Infix "-" := Qp_minus : Qp_scope.
 Infix "*" := Qp_mult : Qp_scope.
 Infix "/" := Qp_div : Qp_scope.
+Notation "1" := Qp_one : Qp_scope.
+Notation "2" := (1 + 1)%Qp : Qp_scope.
+Notation "3" := (1 + 2)%Qp : Qp_scope.
+Notation "4" := (1 + 3)%Qp : Qp_scope.
 
 Lemma Qp_eq x y : x = y â†” Qp_car x = Qp_car y.
 Proof.
-- 
GitLab