# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597805659 -32400
# Node ID a65f3b17eade1c1d47274972fe55408ae9363e25
# Parent  ce6a1a08653ac3f5ec1b9135249c9cb796401685
...

diff -r ce6a1a08653a -r a65f3b17eade Symmetric.agda
--- a/Symmetric.agda	Wed Aug 19 11:28:10 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 11:54:19 2020 +0900
@@ -4,6 +4,7 @@
 open import Algebra
 open import Algebra.Structures
 open import Data.Fin hiding ( _<_  )
+open import Data.Fin.Properties hiding ( <-cmp ; <-trans )
 open import Data.Product
 open import Data.Fin.Permutation
 open import Function hiding (id ; flip)
@@ -131,7 +132,9 @@
           x
        ∎  where
             open ≡-Reasoning
-            lem5 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n))  → p→ x ≡ fromℕ≤ a<sa
+            lem6 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n)) → toℕ x ≡ (suc m)
+            lem6 refl = toℕ-fromℕ≤ _
+            lem5 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n)) → p→ x ≡ fromℕ≤ a<sa
             lem5 refl with <-cmp (toℕ x) m
             lem5 refl | tri< a ¬b ¬c = {!!}
             lem5 refl | tri≈ ¬a refl ¬c = {!!}