# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598699881 -32400
# Node ID 7030fe61274651ce3276aea87ef1dd619f728bf8
# Parent  4efab088abd069a1978583f07a9f207780e96fbc
...

diff -r 4efab088abd0 -r 7030fe612746 Putil.agda
--- a/Putil.agda	Sat Aug 29 12:27:18 2020 +0900
+++ b/Putil.agda	Sat Aug 29 20:18:01 2020 +0900
@@ -177,10 +177,31 @@
    ... | tri≈ ¬a refl ¬c = p13 where
        p13 : fromℕ< (s≤s (s≤s m≤n)) ≡ suc x
        p13 = cong (λ k → suc k ) (fromℕ<-toℕ _ (s≤s m≤n) )
-   ... | tri> ¬a ¬b c = p16 (suc x) where
-       p16 : (x :  Fin (suc (suc n))) → p← x ≡ x
-       p16 zero = {!!}
-       p16 (suc x) = {!!}
+   ... | tri> ¬a ¬b c = p16 (suc x) refl where
+       p16 : (y :  Fin (suc (suc n))) → y ≡ suc x → p← y ≡ suc x
+       p16 zero eq = ⊥-elim ( nat-≡< (cong (λ k → suc (toℕ k) ) eq) (s≤s (s≤s (z≤n))))
+       p16 (suc y) eq with <-cmp (toℕ y) (suc m)   -- suc (suc m) < toℕ (suc x)
+       ... | tri< a ¬b ¬c = p17 where --  x = suc m case
+           p18 : toℕ y ≡ suc (toℕ x) 
+           p18 = begin
+               toℕ y
+              ≡⟨ {!!} ⟩
+                suc (toℕ y)
+              ≡⟨⟩
+                toℕ (suc y)
+              ≡⟨ cong toℕ eq ⟩
+               suc (toℕ x) 
+              ∎
+           p17 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
+           p17 = begin
+                 fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) 
+              ≡⟨ fromℕ<-irrelevant _ _ p18 _ (s≤s (fin<n {suc n} {x})) ⟩ 
+               suc (fromℕ< (fin<n {suc n} {x} )) 
+              ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
+                 suc x
+              ∎
+       ... | tri≈ ¬a b ¬c = eq 
+       ... | tri> ¬a ¬b c₁ = eq 
    ... | tri< a ¬b ¬c = p10 (fromℕ< (≤-trans (s≤s  a) (s≤s (s≤s  m≤n) ))) refl  where
        p10 : (y : Fin (suc (suc n)) ) → y ≡ fromℕ< (≤-trans (s≤s  a) (s≤s (s≤s  m≤n) ))  → p← y ≡ suc x
        p10 zero ()