From 6dc1cfca3c3cf24476c923111f5c9ce803f872b0 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sun, 17 May 2015 12:57:48 +1000
Subject: [PATCH] feat(library/init/nat.lean): add notation <= and >= for nat

---
 library/init/nat.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/library/init/nat.lean b/library/init/nat.lean
index e2c694cca..621df7f7d 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -21,6 +21,7 @@ namespace nat
 
   definition le [reducible] (a b : nat) : Prop := a < succ b
 
+  notation a <= b := le a b
   notation a ≤ b := le a b
 
   definition pred (a : nat) : nat :=
@@ -251,6 +252,7 @@ namespace nat
   definition decidable_ge [instance] : decidable_rel ge :=
   _
 
+  notation a >= b := ge a b
   notation a ≥ b := ge a b
 
   -- add is defined in init.num