--- a/ordinal.agda	Mon Jul 01 19:13:43 2019 +0900
+++ b/ordinal.agda	Tue Jul 02 09:28:26 2019 +0900
@@ -216,17 +216,24 @@
    lemma1 (case1 x) = ¬a x
    lemma1 (case2 x) = ≡→¬d< x
 
-maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
-maxα x y with <-cmp (lv x) (lv y)
+maxα : {n : Level} →  Ordinal {suc n} →  Ordinal  → Ordinal
+maxα x y with trio< x y
 maxα x y | tri< a ¬b ¬c = y
 maxα x y | tri> ¬a ¬b c = x
-maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
+maxα x y | tri≈ ¬a refl ¬c = x
 
-minα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
-minα x y with <-cmp (lv x) (lv y)
+minα : {n : Level} →  Ordinal {suc n} →  Ordinal  → Ordinal
+minα {n} x y with trio< {n} x  y
 minα x y | tri< a ¬b ¬c = x
 minα x y | tri> ¬a ¬b c = y
-minα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = minαd (ord x) (ord y) }
+minα x y | tri≈ ¬a refl ¬c = x
+
+min1 : {n : Level} →  {x y z : Ordinal {suc n} } → z o< x → z o< y → z o< minα x y
+min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y
+min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
+min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
+min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
+
 --
 --  max ( osuc x , osuc y )
 --