# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687482593 -32400
# Node ID f2755eab7b9162dcedfe70a5811c254409514e16
# Parent  aca9b1e6750388d865b56cebd51f187b1ecb4935
...

diff -r aca9b1e67503 -r f2755eab7b91 src/bijection.agda
--- a/src/bijection.agda	Fri Jun 23 08:13:22 2023 +0900
+++ b/src/bijection.agda	Fri Jun 23 10:09:53 2023 +0900
@@ -751,27 +751,31 @@
         ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq
 
     bton : B → ℕ
-    bton b = count-B (fun→ cn (g b))
+    bton b = pred (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 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
+    biso n = begin  
+        bton (ntob n) ≡⟨ refl ⟩
+        pred (count-B (fun→ cn (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (fun→ cn k))) ( CountB.b=cn CB)) ⟩
+        pred (count-B (fun→ cn (fun← cn (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (fiso→ cn _) ⟩
+        pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩
+        pred (suc n) ≡⟨ refl ⟩
+        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 = ?
+    biso1 b = InjectiveF.inject gi ( begin
+        g (ntob (bton b)) ≡⟨ refl ⟩
+        g (CountB.b CB) ≡⟨ sym (CountB.b=cn CB) ⟩
+        ? ≡⟨ ? ⟩
+        g b ∎ ) where
+           open ≡-Reasoning
+           n  = pred (count-B (fun→ cn (g b)))
+           CB = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
 
 bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D)
 bi-∧ {A} {B} {C} {D} ab cd = record {