Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff ordinal.agda @ 113:5f97ebaeb89b

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 Jun 2019 16:04:31 +0900
parents 1daa1d24348c
children 870fe02c7a07
line wrap: on
line diff
--- a/ordinal.agda	Tue Jun 25 05:50:22 2019 +0900
+++ b/ordinal.agda	Tue Jun 25 16:04:31 2019 +0900
@@ -97,6 +97,11 @@
 osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x )
 osuc-lveq {n} = refl
 
+osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox  → osuc oy o< osuc ox
+osucc {n} {ox} {oy} (case1 x) = case1 x
+osucc {n} {ox} {oy} (case2 x) with d<→lv x
+... | refl = case2 (s< x)
+
 nat-<> : { x y : Nat } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x