--- a/Putil.agda	Sat Aug 29 20:18:01 2020 +0900
+++ b/Putil.agda	Sun Aug 30 08:40:31 2020 +0900
@@ -181,25 +181,13 @@
        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 = ⊥-elim ( nat-≡< refl ( ≤-trans c (subst (λ k → k < suc m) p17 a )) ) where
+           --  x = suc m case, c : suc (suc m) ≤ suc (toℕ x), a : suc (toℕ y) ≤ suc m,  suc y ≡ suc x
+           p17 : toℕ y ≡ toℕ x
+           p17 with <-cmp (toℕ y) (toℕ x) | cong toℕ eq
+           ... | tri< a ¬b ¬c | seq =  ⊥-elim ( nat-≡< seq (s≤s a) )
+           ... | tri≈ ¬a b ¬c | seq = b
+           ... | tri> ¬a ¬b c | seq =  ⊥-elim ( nat-≡< (sym seq) (s≤s c))
        ... | 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