# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1695464542 -32400
# Node ID f5b2145c174cf0e4d847615631c7adccfe2ffb54
# Parent  e9ac545595970d19bbadde5aa1b8295b2ba05fb3
...

diff -r e9ac54559597 -r f5b2145c174c src/Putil.agda
--- a/src/Putil.agda	Sat Sep 23 19:12:26 2023 +0900
+++ b/src/Putil.agda	Sat Sep 23 19:22:22 2023 +0900
@@ -294,22 +294,24 @@
 ... | suc t = p012 where
     p003 : 0 < toℕ (Inverse.to perm zero)
     p003 = subst ( λ k → 0 < k ) (cong toℕ (sym eq)) (s≤s z≤n)
+    p008 : toℕ (Data.Fin.pred (Inverse.to perm zero)) ≡ toℕ (Inverse.to perm zero) ∸ 1
+    p008 = ?
     p002 : toℕ (Inverse.to perm zero) ≤ suc n
     p002 = toℕ≤pred[n] (Inverse.to perm zero)
     p001 : suc (toℕ (Data.Fin.pred (Inverse.to perm zero))) ≤ suc n
     p001 = begin
-        suc (toℕ (Data.Fin.pred (Inverse.to perm zero)))  ≡⟨  {!!} ⟩
+        suc (toℕ (Data.Fin.pred (Inverse.to perm zero)))  ≡⟨ cong suc p008  ⟩
         suc (Data.Nat.pred (toℕ (Inverse.to perm zero)))  ≡⟨ sucprd p003 ⟩
         toℕ (Inverse.to perm zero)  ≤⟨ p002 ⟩
         suc n  ∎ where open ≤-Reasoning
-    p007 : Data.Nat.pred (suc (toℕ (Inverse.to perm zero))) < suc n
-    p007 = ?
+    p007 : Data.Nat.pred (toℕ (Inverse.to perm zero)) < suc n
+    p007 = subst (λ k → k < suc n ) p008 ?
     p012 : Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] (suc t))) zero) ≡ # 0 
     p012 = begin
-        Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] (suc t))) zero) ≡⟨ ? ⟩ 
+        Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] (suc t))) zero) ≡⟨ cong (λ k → perm ∘ₚ flip (pins (toℕ≤pred[n] k)) ⟨$⟩ˡ # 0) (sym eq) ⟩ 
         perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ # 0))) ⟨$⟩ˡ # 0 ≡⟨ p011 _ _ perm p001 (s≤s z≤n) ⟩
-        perm ⟨$⟩ˡ suc (fromℕ< p001) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (lemma10 ?) ⟩
-        perm ⟨$⟩ˡ suc (fromℕ< ?) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (pred-fin (Inverse.to perm zero) p003 ? ) ⟩
+        perm ⟨$⟩ˡ suc (fromℕ< p001) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (lemma10 (cong suc p008)) ⟩
+        perm ⟨$⟩ˡ suc (fromℕ< p007) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (pred-fin (Inverse.to perm zero) p003 p007 ) ⟩
         perm ⟨$⟩ˡ (Inverse.to perm zero) ≡⟨ inverseˡ perm  ⟩
         # 0 ∎ where 
             open ≡-Reasoning