Mercurial > hg > Members > kono > Proof > galois

diff nat.agda @ 91:482ef04890f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 29 Aug 2020 07:48:45 +0900
parents 69ed81f8e212
children 43731a549950
line wrap: on
line diff
--- a/nat.agda	Fri Aug 28 22:20:39 2020 +0900
+++ b/nat.agda	Sat Aug 29 07:48:45 2020 +0900
@@ -34,6 +34,10 @@
 refl-≤s {zero} = z≤n
 refl-≤s {suc x} = s≤s (refl-≤s {x})
 
+a≤sa : {x : ℕ } → x ≤ suc x
+a≤sa {zero} = z≤n
+a≤sa {suc x} = s≤s (a≤sa {x})
+
 =→¬< : {x : ℕ  } → ¬ ( x < x )
 =→¬< {zero} ()
 =→¬< {suc x} (s≤s lt) = =→¬< lt