--- a/automaton-in-agda/src/root2.agda	Tue Jun 29 16:10:06 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Tue Jun 29 18:37:42 2021 +0900
@@ -54,16 +54,24 @@
        2 * (n * n)  ≡⟨ sym (*-assoc 2 n n)  ⟩
        (2 * n) * n ≡⟨ 2nm  ⟩
        m * m ∎ }  where open ≡-Reasoning
+     -- 2 * n * n = 2m' 2m'
+     --  n * n = m' 2m'
     df = Dividable.factor dm
     dn : Dividable 2 n
-    dn = divdable^2 n 2 a<sa n>1 p2 record { factor = Dividable.factor dm * m ; is-factor = begin
-        df * m * 2 + 0  ≡⟨ *-cancelʳ-≡ _ _ {1} ( begin 
-          {!!}  ≡⟨  {!!} ⟩
-          ((df * m) * 2 )  ≡⟨  {!!} ⟩
-          ((m * df) * 2 )  ≡⟨  {!!} ⟩
-          (m * (df * 2) )  ≡⟨  {!!} ⟩
-          (m * (df * 2 + 0) )  ≡⟨  {!!} ⟩
-          m * m   ≡⟨  {!!} ⟩
+    dn = divdable^2 n 2 a<sa n>1 p2 record { factor = df * df  ; is-factor = begin
+        df * df * 2 + 0  ≡⟨ *-cancelʳ-≡ _ _ {1} ( begin 
+          (df * df * 2 + 0) * 2 ≡⟨  cong (λ k → k * 2)  (+-comm (df * df * 2) 0)  ⟩
+          ((df * df) * 2) * 2 ≡⟨ cong (λ k → k * 2) (*-assoc df df 2 ) ⟩
+          (df * (df * 2)) * 2 ≡⟨ cong (λ k → (df * k ) * 2) (*-comm df 2)  ⟩
+          (df * (2 * df)) * 2 ≡⟨ sym ( cong (λ k → k * 2) (*-assoc df 2 df ) ) ⟩
+          ((df * 2) * df) * 2 ≡⟨ *-assoc (df * 2) df 2  ⟩
+          (df * 2) * (df * 2) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * 2)) (+-comm 0 _) ⟩
+          (df * 2 + 0) * (df * 2 + 0)   ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
+          m * m   ≡⟨ sym 2nm ⟩
+          2 * n * n   ≡⟨ cong (λ k → k * n) (*-comm 2 n) ⟩
+          n * 2 * n   ≡⟨ *-assoc n 2 n ⟩
+          n * (2 * n)   ≡⟨ cong (λ k → n * k) (*-comm 2 n) ⟩
+          n * (n * 2)   ≡⟨ sym (*-assoc n n 2) ⟩
           n * n * 2 ∎  ) ⟩
        n * n ∎ }  where open ≡-Reasoning