# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687387109 -32400
# Node ID 8b66575d4939dcfcc084eba0db9a234307860821
# Parent  3bcff593255e4aac1fb28181b97c7e1e77e7b5fa
lem06

diff -r 3bcff593255e -r 8b66575d4939 src/bijection.agda
--- a/src/bijection.agda	Wed Jun 21 17:05:15 2023 +0900
+++ b/src/bijection.agda	Thu Jun 22 07:38:29 2023 +0900
@@ -685,26 +685,37 @@
          --  induction on n is no good, because (ani (suc n)) may happen in clist (c n)
          --  so we cannot recurse on n<ca-list itself.
          --
+
          del : (i : ℕ) → (cl : List C) → any-cl i cl → List C   -- del 0 contains ani 0
-         del = ?
+         del i cl a = a-list i cl (a i ≤-refl)  
          del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl)  → any-cl i (del (suc i) cl a )
-         del-any = ?
+         del-any i cl a j le = lem41 cl (del (suc i) cl a ) (a (suc i) ≤-refl ) (a j (≤-trans le a≤sa) ) refl where
+            lem41 : (cl dl : List C) 
+                 → (ai : Any (_≡_ (g (f (fun← an (suc i))))) cl)
+                 → (aj : Any (_≡_ (g (f (fun← an j)))) cl) 
+                 → dl ≡ a-list (suc i) cl ai →   Any (_≡_ (g (f (fun← an j)))) dl
+            lem41 (h ∷ t) y (here px) (here px₁) eq = ⊥-elim ( nat-≡< 
+                 (  bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) (x≤y→x<sy le) )
+            lem41 (h ∷ t) y (here px) (there b0) eq = subst (λ k →  Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b0
+            lem41 (h ∷ t) y (there a0) (here px) refl = here px
+            lem41 (h ∷ t) (x ∷ y) (there a0) (there b0) refl = there (lem41 t (a-list (suc i) t a0) a0 b0 refl)
+
          del-ca : (i : ℕ) → (cl : List C) → (a : any-cl i cl  )
-              → suc (ca-list cl) ≡ ca-list (del i cl a)
-         del-ca = ?
+              → suc (ca-list (del i cl a)) ≡ ca-list cl
+         del-ca i cl a = a-list-ca i cl (a i ≤-refl) 
+
          lem06 : suc n < ca-list (clist (c (suc n)))
          lem06 = lem31 where
             lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → suc i < ca-list cl
             lem30 0 cl i≤n a = begin
                 2 ≤⟨ s≤s (s≤s z≤n) ⟩ 
-                suc (suc (ca-list (del 0 (del 1 cl a) (del-any 0 cl a)) ))  ≡⟨ cong suc ( del-ca 0 (del 1 cl a) (del-any 0 cl a) )  ⟩ 
+                suc (suc (ca-list (del 0 (del 1 cl a) (del-any 0 cl a)) )) ≡⟨ cong suc ( del-ca 0 (del 1 cl a) (del-any 0 cl a)) ⟩ 
                 suc (ca-list (del 1 cl a) )  ≡⟨ del-ca 1 cl a ⟩ 
                 ca-list cl ∎ where
                    open ≤-Reasoning
             lem30 (suc i) cl i≤n a = begin
-               suc (suc (suc i))   ≤⟨ s≤s (lem30 i (del (suc i) (del (suc (suc i)) cl a )  
-                    (del-any (suc i) cl a)  ) (≤-trans a≤sa i≤n) (del-any (suc i) cl a)) ⟩ 
-               suc (ca-list (del (suc i) cl (del-any (suc i) cl a)))  ≡⟨ del-ca (suc i) cl (del-any (suc i) cl a) ⟩ 
+               suc (suc (suc i))   ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any (suc i) cl a) ) ⟩ 
+               suc (ca-list (del (suc (suc i)) cl a))  ≡⟨ del-ca (suc (suc i)) cl a ⟩ 
                ca-list cl ∎ where
                    open ≤-Reasoning
             lem31 : suc n < ca-list (clist (c (suc n)))
diff -r 3bcff593255e -r 8b66575d4939 src/nat.agda
--- a/src/nat.agda	Wed Jun 21 17:05:15 2023 +0900
+++ b/src/nat.agda	Thu Jun 22 07:38:29 2023 +0900
@@ -280,6 +280,10 @@
 x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le)
 x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl
 
+x≤y→x<sy : {x y : ℕ } → x ≤ y → x < suc y 
+x≤y→x<sy {.zero} {y} z≤n = ≤-trans a<sa (s≤s z≤n)
+x≤y→x<sy {.(suc _)} {.(suc _)} (s≤s le) = s≤s ( x≤y→x<sy le) 
+
 
 open import Data.Product