Mercurial > hg > Members > kono > Proof > galois

changeset 29:a65f3b17eade

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Aug 2020 11:54:19 +0900
parents ce6a1a08653a
children a9fa68dfbd26
files Symmetric.agda
diffstat 1 files changed, 4 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}