--- a/sym5.agda	Mon Aug 24 18:55:37 2020 +0900
+++ b/sym5.agda	Mon Aug 24 20:01:18 2020 +0900
@@ -26,6 +26,8 @@
    open Solvable (Symmetric 2)
    -- open Group (Symmetric 2) using (_⁻¹)
 
+   f2-⊥ : (x : Fin 2 ) → x ≡ zero → x ≡ suc zero → ⊥
+   f2-⊥ x refl ()
    s2 :  ( g : Permutation 2 2 ) → g =p= pinv g 
    s2 g = record { peq = λ q → s2lem q } where
       s2lem : (q : Fin 2) → (g ⟨$⟩ʳ q) ≡ (pinv g ⟨$⟩ʳ q)
@@ -39,25 +41,35 @@
           ≡⟨⟩
              pinv g ⟨$⟩ʳ zero
           ∎ where open ≡-Reasoning
-      s2lem zero | suc zero | record { eq = e2 }  = begin
-             suc zero
-          ≡⟨ {!!} ⟩
-             g ⟨$⟩ʳ zero
-          ≡⟨ {!!} ⟩
-             g ⟨$⟩ˡ (g ⟨$⟩ʳ ( g ⟨$⟩ˡ zero ))
-          ≡⟨ {!!} ⟩
-             g ⟨$⟩ˡ zero
-          ≡⟨⟩
-             pinv g ⟨$⟩ʳ zero
+      s2lem zero | suc zero | record { eq = e2 }  = sym shlem1 where
+         shlem1 :  pinv g ⟨$⟩ʳ zero ≡ suc zero
+         shlem1 with g ⟨$⟩ˡ zero | inspect  (_⟨$⟩ˡ_ g ) zero | inverseʳ g {zero}
+         shlem1 | zero | record { eq = e1 } | u = ⊥-elim  (f2-⊥ _ u e2 )
+         shlem1 | suc zero | s | u = refl
+      s2lem (suc zero) with g ⟨$⟩ʳ suc zero | inspect  (_⟨$⟩ʳ_ g ) (suc zero)
+      s2lem (suc zero) | zero | record { eq = e1 }  = sym shlem2 where
+         shlem2 :  pinv g ⟨$⟩ʳ suc zero ≡ zero
+         shlem2 with g ⟨$⟩ˡ suc zero | inspect  (_⟨$⟩ˡ_ g ) (suc zero ) | inverseʳ g {suc zero}
+         shlem2 | suc zero | record { eq = e2 } | u = ⊥-elim  (f2-⊥ _ e1 u )
+         shlem2 | zero | s | u = refl
+      s2lem (suc zero) | suc zero | record { eq = e2 }  = begin
+              suc zero
+          ≡⟨ sym (inverseˡ g ) ⟩
+             g ⟨$⟩ˡ ( g ⟨$⟩ʳ suc zero )
+          ≡⟨ cong ( λ k →  g ⟨$⟩ˡ k ) e2 ⟩
+             pinv g ⟨$⟩ʳ suc zero
           ∎ where open ≡-Reasoning
-      s2lem (suc zero) = {!!} 
 
    sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-   sym2lem0 g h q with perm→FL g | perm→FL h
-   sym2lem0 g h q | zero :: (zero :: f0) | zero :: (zero :: f0) = {!!}
-   sym2lem0 g h q | zero :: (zero :: f0) | suc zero :: (zero :: f0) = {!!}
-   sym2lem0 g h q | suc zero :: (zero :: f0) | zero :: (zero :: f0) = {!!}
-   sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) = {!!}
+   sym2lem0 g h q = begin
+             [ g , h ]  ⟨$⟩ʳ q
+          ≡⟨⟩
+              h ⟨$⟩ʳ ( g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q )))
+          ≡⟨ {!!} ⟩
+             q
+          ≡⟨⟩
+             pid ⟨$⟩ʳ q
+          ∎ where open ≡-Reasoning
    solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
    solved x uni = prefl
    solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h  }