From 8fda19cb580bda72f374bc2176d7e2efa5cd613b Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Sun, 28 Jun 2020 15:06:17 +0100
Subject: Work on proof.

---
 src/common/Coquplib.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/common/Coquplib.v')

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index b4ca906..b8a02d2 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -117,6 +117,9 @@ Ltac simplify := unfold_constants; simpl in *;
 Global Opaque Nat.div.
 Global Opaque Z.mul.
 
+Infix "==nat" := eq_nat_dec (no associativity, at level 50).
+Infix "==Z" := Z.eq_dec (no associativity, at level 50).
+
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
-- 
cgit