# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686404565 -32400
# Node ID 46d2c0341fcbd36c64818275a0ec4605bb4bc37a
# Parent  c7623ec8f0d33b68d1eafeed51fe68a389b2282d
...

diff -r c7623ec8f0d3 -r 46d2c0341fcb src/bijection.agda
--- a/src/bijection.agda	Sat Jun 10 21:27:39 2023 +0900
+++ b/src/bijection.agda	Sat Jun 10 22:42:45 2023 +0900
@@ -610,6 +610,16 @@
                 --
                 nac : ℕ
                 nac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j))
+                n<ca : suc j < count-A nac
+                n<ca = ? where
+                    n<ca1 : (i n : ℕ ) → i ≤ suc j → n ≤ nac  →  i < count-A n
+                    n<ca1 zero n with is-A (fun← cn zero)
+                    ... | yes isa = ?
+                    ... | no nisa = ?
+                    n<ca1 (suc i) n with is-A (fun← cn (suc i))
+                    ... | yes isa = ? -- n<ca1 ?
+                    ... | no nisa = ? -- n<ca1 ?
+
 
     lem01 : (n i : ℕ) → n < count-B i → B
     lem01 zero zero lt with is-B (fun← cn zero)
@@ -626,6 +636,26 @@
     ... | tri≈ ¬a b ¬c = Is.a isB
     ... | tri> ¬a ¬b c = ? -- cannot happen
 
+    record CountB (n : ℕ) : Set where
+       field
+          b : B
+          cb : ℕ
+          b=cn : fun← cn cb ≡ g b
+          cb=n : count-B cb ≡ n
+
+    lem011 : (n i : ℕ) → n ≤ count-B i → CountB n
+    lem011 zero zero z≤n with is-B (fun← cn zero)
+    ... | no nisB = ?
+    ... | yes isB = ?
+    lem011 (suc n) zero ()
+    lem011 n (suc i) n≤i with is-B (fun← cn (suc i))
+    ... | no nisB = lem011 n i n≤i
+    ... | yes isB with <-cmp (count-B (suc i)) n
+    ... | tri< a ¬b ¬c = lem011 n i ?
+    ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = eq }
+    ... | tri> ¬a ¬b c = lem011 n i ?
+
+
     ntob : (n : ℕ) → B
     ntob n = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )