--- a/Symmetric.agda	Wed Aug 19 19:55:32 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 23:23:07 2020 +0900
@@ -3,8 +3,8 @@
 open import Level hiding ( suc ; zero )
 open import Algebra
 open import Algebra.Structures
-open import Data.Fin hiding ( _<_  )
-open import Data.Fin.Properties hiding ( <-cmp ; <-trans )
+open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ )
+open import Data.Fin.Properties hiding ( <-cmp ; <-trans ; ≤-trans )
 open import Data.Product
 open import Data.Fin.Permutation
 open import Function hiding (id ; flip)
@@ -92,23 +92,11 @@
 
    piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x
    piso← zero = refl
-   piso← (suc x) = begin
-          p→ (p← (suc x)) 
-       ≡⟨⟩
-         suc (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ x))
-       ≡⟨ cong (λ k → suc k ) (inverseˡ perm) ⟩
-          suc x
-       ∎ where open ≡-Reasoning
+   piso← (suc x) = cong (λ k → suc k ) (inverseˡ perm) 
 
    piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
    piso→ zero = refl
-   piso→ (suc x) = begin
-          p← (p→ (suc x)) 
-       ≡⟨⟩
-         suc (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ x))
-       ≡⟨ cong (λ k → suc k ) (inverseʳ perm) ⟩
-          suc x
-       ∎ where open ≡-Reasoning
+   piso→ (suc x) = cong (λ k → suc k ) (inverseʳ perm) 
 
 pswap  : {n : ℕ }  → Permutation n n → Permutation (suc (suc n)) (suc (suc  n ))
 pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
@@ -125,24 +113,12 @@
    piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
    piso← zero = refl
    piso← (suc zero) = refl
-   piso← (suc (suc x)) = begin
-          p→ (p← (suc (suc x)))
-       ≡⟨⟩
-         suc ( suc (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ x)))
-       ≡⟨ cong (λ k → suc (suc k) ) (inverseˡ perm) ⟩
-          suc (suc x)
-       ∎ where open ≡-Reasoning
+   piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) 
 
    piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
    piso→ zero = refl
    piso→ (suc zero) = refl
-   piso→ (suc (suc x)) = begin
-          p← (p→ (suc (suc x)) )
-       ≡⟨⟩
-         suc (suc (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ x)))
-       ≡⟨ cong (λ k → suc (suc k) ) (inverseʳ perm) ⟩
-          suc (suc x)
-       ∎ where open ≡-Reasoning
+   piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) 
 
 -- enumeration
 
@@ -150,10 +126,17 @@
 psawpn {suc zero} {m} (s≤s ())
 psawpn {suc n} {m} (s≤s (s≤s x)) = pswap pid 
 
-pfill : {n m : ℕ} → m < n → Permutation m m → Permutation n n
-pfill = {!!}
+pfill : { n m : ℕ } → m ≤ n → Permutation  m m → Permutation n n
+pfill {n} {m} m≤n perm = pfill1 (n - m) (n-m<n n m ) (subst (λ k → Permutation k k ) (n-n-m=m m≤n ) perm) where
+   pfill1 : (i : ℕ ) → i ≤ n  → Permutation (n - i) (n - i)  →  Permutation n n
+   pfill1 0 _ perm = perm
+   pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) )
 
 eperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
 eperm {zero} ()
-eperm {suc n} {0} (s≤s z≤n) perm = pprep perm
-eperm {suc (suc n)} {suc m} (s≤s (s≤s m<n)) perm = {!!}
+eperm {n} {0} (s≤s z≤n) perm = pprep perm
+eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 {!!} (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 )
+    eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) {!!} (pprep sw) perm
+