Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/nat.agda @ 923:85f6238a38db
use supf of zchain for (nmx : ¬ Maximal A ) → ⊥
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 19 Oct 2022 08:41:42 +0900 |
parents | 81691a6b352b |
children | a27f28dbed87 |
line wrap: on
line source
module nat where open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Data.Empty open import Relation.Nullary open import Relation.Binary.PropositionalEquality open import logic nat-<> : { x y : Nat } → x < y → y < x → ⊥ nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥ nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x nat-<≡ : { x : Nat } → x < x → ⊥ nat-<≡ (s≤s lt) = nat-<≡ lt nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ nat-≡< refl lt = nat-<≡ lt ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ ¬a≤a (s≤s lt) = ¬a≤a lt a<sa : {la : Nat} → la < Suc la a<sa {Zero} = s≤s z≤n a<sa {Suc la} = s≤s a<sa <to≤ : {x y : Nat } → x < y → x ≤ y <to≤ {Zero} {Suc y} (s≤s z≤n) = z≤n <to≤ {Suc x} {Suc y} (s≤s lt) = s≤s (<to≤ {x} {y} lt) =→¬< : {x : Nat } → ¬ ( x < x ) =→¬< {Zero} () =→¬< {Suc x} (s≤s lt) = =→¬< lt >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x <-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) ) <-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl <-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n) <-∨ {Suc x} {Zero} (s≤s ()) <-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt <-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq) <-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) max : (x y : Nat) → Nat max Zero Zero = Zero max Zero (Suc x) = (Suc x) max (Suc x) Zero = (Suc x) max (Suc x) (Suc y) = Suc ( max x y )