# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686264151 -32400
# Node ID 71652ee117a744e89b634d6c9f7c0396da95bc93
# Parent  4ad33efd8486e57e4aa16bfb7a7fddfb4f7ae8f8
...

diff -r 4ad33efd8486 -r 71652ee117a7 src/bijection.agda
--- a/src/bijection.agda	Thu Jun 08 18:18:15 2023 +0900
+++ b/src/bijection.agda	Fri Jun 09 07:42:31 2023 +0900
@@ -558,19 +558,20 @@
     cbn n = fun→ cn (g (f (fun← an n)))
 
     cb< : (n : ℕ) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n)))
-    cb< n = ? where
-        cb00 : (i : ℕ) → i ≤ CB.cb (lb (cbn (suc n))) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n)))
-        cb00 i i≤csn with inspect cbn (suc n) | lb (cbn (suc n)) 
-        cb00 zero lt | record {eq = eq1 } | s with is-A (fun← cn (cbn 0)) | is-B (fun← cn (cbn 0))
+    cb< n = cb00 (CB.cb (lb (cbn n))) ≤-refl  where
+        cb00 : (i : ℕ) → i ≤ CB.cb (lb (cbn n)) → i < CB.cb (lb (cbn (suc n))) 
+        cb00 zero le with is-A (fun← cn (cbn 0)) | is-B (fun← cn (cbn 0))
         ... | yes isA | yes isB = ?
         ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
         ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl )   } )
         ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl )   } )
-        cb00 (suc c) lt | record {eq = eq1 } | s with is-A (fun← cn (suc c)) | is-B (fun← cn (suc c))
-        ... | yes isA | yes isB = ? -- <-transʳ z≤n ≤-refl 
+        cb00 (suc c) le with is-A (fun← cn (suc c)) | is-B (fun← cn (suc c))
+        ... | yes isA | yes isB = ? where -- <-transʳ z≤n ≤-refl 
+             cb01 : c < CB.cb (lb (cbn (suc n))) 
+             cb01 = cb00 c (sx≤y→x≤y le)
         ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-        ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  ? )   } )
-        ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  ? )   } )
+        ... | no nisA | yes isB = ?
+        ... | no nisA | no nisB = ?
 
     cb<0 : 0 < CB.cb (lb (cbn 0))
     cb<0 with cbn 0 | inspect cbn 0
diff -r 4ad33efd8486 -r 71652ee117a7 src/nat.agda
--- a/src/nat.agda	Thu Jun 08 18:18:15 2023 +0900
+++ b/src/nat.agda	Fri Jun 09 07:42:31 2023 +0900
@@ -45,6 +45,14 @@
 <-∨ {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)
 
+≤-∨ : { x y : ℕ } → x ≤ y → ( (x ≡ y ) ∨ (x < y) )
+≤-∨ {zero} {zero} z≤n = case1 refl
+≤-∨ {zero} {suc y} z≤n = case2 (s≤s z≤n)
+≤-∨ {suc x} {zero} ()
+≤-∨ {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 : ℕ) → ℕ
 max zero zero = zero
 max zero (suc x) = (suc x)
@@ -226,6 +234,10 @@
 px≤py {zero} {suc y} lt = z≤n
 px≤py {suc x} {suc y} (s≤s lt) = lt 
 
+sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x  ≤ y 
+sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n
+sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le)
+
 open import Data.Product
 
 i-j=0→i=j : {i j  : ℕ } → j ≤ i  → i - j ≡ 0 → i ≡ j