# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687404369 -32400
# Node ID 1da09696a2564ac22896e65e2ab447bd1ebc453f
# Parent  4b7a756dae330ee1fff481268705166c44cd96d7
...

diff -r 4b7a756dae33 -r 1da09696a256 src/bijection.agda
--- a/src/bijection.agda	Thu Jun 22 09:20:17 2023 +0900
+++ b/src/bijection.agda	Thu Jun 22 12:26:09 2023 +0900
@@ -731,24 +731,19 @@
           cb=n : count-B cb ≡ suc n
 
     lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
-    lem01 zero zero le with is-B (fun← cn 0) | inspect count-B zero
-    ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = eq1 } 
-    ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≤> le a<sa)
-    lem01 zero (suc i) le  with ≤-∨ le
-    ... | case1 eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-    ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 (sym eq) } 
-    ... | no nisb | record { eq = eq1 } = lem01 zero i le
-    lem01 zero (suc i) le  | case2 lt with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-    ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 ? }
-    ... | no nisb | record { eq = eq1 } = lem01 zero i le
-    lem01 (suc n) zero ()
-    lem01 (suc n) (suc i) n≤i with is-B (fun← cn (suc i))
-    ... | no nisB = lem01 (suc n) i n≤i
-    ... | yes isB with <-cmp (count-B (suc i)) (suc n)
-    ... | tri< a ¬b ¬c = lem01 (suc n) i ?
-    ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = ? }
-    ... | tri> ¬a ¬b c = lem01 (suc n) i ?
-
+    lem01 n i le = ? where
+        -- starting from 0, if count B i ≡ suc n, this is it
+        lem03 : (i m : ℕ ) → i ≤ m → count-B i < count-B m → CountB i
+        lem03 0 0 i≤m ci<cm  = ⊥-elim ( nat-≡< refl ci<cm )
+        lem03 0 (suc m) i≤m ci<cm  with is-B (fun← cn (suc m)) | inspect count-B (suc m)
+        ... | yes isb | record { eq = eq1 } with <-cmp 0 (count-B m)
+        ... | tri≈ ¬a cb=0 ¬c = record { b = Is.a isb ; cb = suc m ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 (cong suc (sym cb=0)) }
+        ... | tri< 0<cb ¬b ¬c with count-B m | inspect count-B m
+        ... | 0 | record { eq = eq2 } = record { b = Is.a isb ; cb = suc m ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 refl }
+        ... | suc cb | record { eq = eq2 } = lem03 0 m z≤n  (subst (λ k → _ < k ) (sym eq2) (x≤y→x<sy ?) )
+        lem03 zero (suc m) z≤n ci<cm | no nisb | record { eq = eq1 } = lem03 0 m z≤n (<-transˡ a<sa ci<cm)
+        lem03 (suc i) 0 i≤m ci<cm  = ?
+        lem03 (suc i) (suc m) i≤m ci<cm  = ?
 
     ntob : (n : ℕ) → B
     ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ))