Mercurial > hg > Members > kono > Proof > galois

comparison nat.agda @ 74:69ed81f8e212

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 Tue, 25 Aug 2020 14:15:49 +0900
parents 09fa2ab75703
children 482ef04890f8
comparison
equal deleted inserted replaced
73:9bd1d7cd432c 74:69ed81f8e212
5 open import Data.Nat.Properties 5 open import Data.Nat.Properties
6 open import Data.Empty 6 open import Data.Empty
7 open import Relation.Nullary 7 open import Relation.Nullary
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 open import Relation.Binary.Core 9 open import Relation.Binary.Core
10 open import Relation.Binary.Definitions
10 open import logic 11 open import logic
11 12
12 13
13 nat-<> : { x y : ℕ } → x < y → y < x → ⊥ 14 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
14 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x 15 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x