--- a/src/bijection.agda	Thu Jun 22 18:15:14 2023 +0900
+++ b/src/bijection.agda	Fri Jun 23 08:13:22 2023 +0900
@@ -536,9 +536,6 @@
     ... | yes isb = suc (count-B n)
     ... | no nisb = count-B n
 
-    bton : B → ℕ
-    bton b = count-B (fun→ cn (g b))
-
     count-A : ℕ → ℕ
     count-A zero with is-A (fun← cn zero)
     ... | yes isb = 1
@@ -731,7 +728,7 @@
           cb=n : count-B cb ≡ suc n
 
     lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
-    lem01 n i le = ? where
+    lem01 n i le = lem09 i (count-B i) le refl where
         -- starting from 0, if count B i ≡ suc n, this is it
         lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
         lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0
@@ -741,25 +738,37 @@
         ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq} 
         ... | no nisb | record { eq = eq1 } = lem07 n i  eq
 
-        lem08 : (i : ℕ) → suc n ≤ count-B i →  CountB n
-        lem08 0 n<cb with is-B (fun← cn i)| inspect count-B 0
-        ... | no nisb | record { eq = eq1 } = ?
-        ... | yes isb | record { eq = eq1 } with <-cmp (count-B i) 0
-        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (s≤s z≤n ))
-        ... | tri≈ ¬a b ¬c = record { b = Is.a isb ; cb = i ; b=cn = sym (Is.fa=c isb) ; cb=n = ? }
-        ... | tri> ¬a ¬b c₁ = ?
-        lem08 (suc i) n<cb with is-B (fun← cn (suc i))| inspect count-B (suc i)
-        ... | no nisb | record { eq = eq1 } = lem08 i n<cb
-        ... | yes isb | record { eq = eq1 } with <-cmp (count-B i) (suc n)
-        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a ?)
-        ... | tri≈ ¬a b ¬c = lem07 n i b
-        ... | tri> ¬a ¬b c₁ = lem08 i (≤-trans a≤sa c₁)
+        lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i →  CountB n
+        lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
+        ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
+        ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n))
+        lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq ))
+        ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+        ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq)
+        ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq
+
+    bton : B → ℕ
+    bton b = count-B (fun→ cn (g b))
 
     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))) ))
 
     biso : (n : ℕ) → bton (ntob n) ≡ n
-    biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl
+    biso 0 = ?
+    biso (suc n) = begin  -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl
+        bton (ntob (suc n)) ≡⟨ ? ⟩
+        count-B (fun→ cn (g (CountB.b CB1))) ≡⟨ sym ( cong (λ k → count-B (fun→ cn k)) ( CountB.b=cn CB1)) ⟩
+        count-B (fun→ cn (fun← cn (CountB.cb CB1))) ≡⟨ ? ⟩
+        count-B (CountB.cb CB1) ≡⟨ CountB.cb=n CB1 ⟩
+        ? ≡⟨ ? ⟩
+        suc n ∎ where
+           open ≡-Reasoning
+           CB  = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
+           CB1 = lem01 (suc n) (maxAC.ac (lem02 (suc n))) (≤-trans (maxAC.n<ca (lem02 (suc n))) (ca≤cb0 (maxAC.ac (lem02 (suc n)))) )
+
 
     biso1 : (b : B) → ntob (bton b) ≡ b
     biso1 b = ?

--- a/src/nat.agda	Thu Jun 22 18:15:14 2023 +0900
+++ b/src/nat.agda	Fri Jun 23 08:13:22 2023 +0900
@@ -248,6 +248,9 @@
 refl-≤ {zero} = z≤n
 refl-≤ {suc x} = s≤s (refl-≤ {x})
 
+refl-≤≡ : {x y : ℕ } → x ≡ y → x ≤ y
+refl-≤≡ refl = refl-≤ 
+
 x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
 x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
 x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)