--- a/Symmetric.agda	Wed Aug 19 23:31:48 2020 +0900
+++ b/Symmetric.agda	Thu Aug 20 00:26:38 2020 +0900
@@ -3,7 +3,7 @@
 open import Level hiding ( suc ; zero )
 open import Algebra
 open import Algebra.Structures
-open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ )
+open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ )
 open import Data.Fin.Properties hiding ( <-cmp ; <-trans ; ≤-trans )
 open import Data.Product
 open import Data.Fin.Permutation
@@ -135,8 +135,35 @@
 eperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
 eperm {zero} ()
 eperm {n} {0} (s≤s z≤n) perm = pprep perm
-eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 (s≤s (s≤s (z≤n)))  (pswap {0} pid ) (pprep perm) where
-    eperm1 : (m i : ℕ ) → i ≤ suc (suc m)  → Permutation i i → Permutation (suc n)(suc n)→ Permutation (suc n)(suc n)
-    eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill {!!} sw )  -- i ≤ suc (suc n)
-    eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) {!!} (pprep sw) perm
+eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pswap {0} pid ) (pprep perm) where
+    lemm3 : 2 + m ≤ suc n
+    lemm3 = ≤-trans (s≤s m<n) refl-≤s
+    eperm1 : (m i : ℕ ) → i + m ≤ suc n  → Permutation i i → Permutation (suc n)(suc n)→ Permutation (suc n)(suc n)
+    eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill (subst (λ k → k ≤ suc n) (+-comm i _) i<ssm) sw )  -- i + zero ≤ suc (suc n) → i ≤ suc (suc n)
+    eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) (lemm4 i<ssm ) (pprep sw) perm where
+       lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n
+       lemm4 lt = begin
+          suc i + m  ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩
+          suc m + i  ≡⟨ +-comm (suc m)  _  ⟩
+          i + suc m  ≤⟨ lt ⟩
+          suc n
+        ∎   where open  ≤-Reasoning
+
 
+finpid : (n i : ℕ ) → i < n → List (Fin n)
+finpid (suc n) zero _ = fromℕ≤ {zero} (s≤s z≤n) ∷ []
+finpid (suc n) (suc i) (s≤s lt) = fromℕ≤ (s≤s lt) ∷ finpid (suc n) i (<-trans lt a<sa) 
+
+fpid : (n : ℕ ) → List (Fin n)
+fpid 0 = []
+fpid (suc j) = finpid (suc j) j a<sa where
+
+plist  : {n  : ℕ} → Permutation n n → List ℕ
+plist {0} perm = []
+plist {suc j} perm = plist1 j a<sa where
+    n = suc j
+    plist1 : (i : ℕ ) → i < n → List ℕ
+    plist1  zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
+    plist1  (suc i) (s≤s lt) = toℕ (  perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1  i (<-trans lt a<sa) 
+
+test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )