Mercurial > hg > Members > kono > Proof > galois

comparison 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
comparison
equal deleted inserted replaced
90:bb8c5b366219 91:482ef04890f8
31 a<sa {suc la} = s≤s a<sa 31 a<sa {suc la} = s≤s a<sa
32 32
33 refl-≤s : {x : ℕ } → x ≤ suc x 33 refl-≤s : {x : ℕ } → x ≤ suc x
34 refl-≤s {zero} = z≤n 34 refl-≤s {zero} = z≤n
35 refl-≤s {suc x} = s≤s (refl-≤s {x}) 35 refl-≤s {suc x} = s≤s (refl-≤s {x})
36
37 a≤sa : {x : ℕ } → x ≤ suc x
38 a≤sa {zero} = z≤n
39 a≤sa {suc x} = s≤s (a≤sa {x})
36 40
37 =→¬< : {x : ℕ } → ¬ ( x < x ) 41 =→¬< : {x : ℕ } → ¬ ( x < x )
38 =→¬< {zero} () 42 =→¬< {zero} ()
39 =→¬< {suc x} (s≤s lt) = =→¬< lt 43 =→¬< {suc x} (s≤s lt) = =→¬< lt
40 44