# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1642167580 -32400
# Node ID 7f806a28a8662ecee276d1cbb7cb9efc2553e428
# Parent  596913103389ec6f621dfdad6f8d0b7f87ebfe5b
...

diff -r 596913103389 -r 7f806a28a866 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Fri Jan 14 21:47:24 2022 +0900
+++ b/automaton-in-agda/src/root2.agda	Fri Jan 14 22:39:40 2022 +0900
@@ -200,15 +200,23 @@
      r00 : p * j * j ≡ i * i
      r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
      r01 : p ≡ i * i
-     r01 = {!!} 
-     r02 : (i : ℕ) → p ≡ i * i → gcd p i ≡ i 
-     r02 = {!!}
+     r01 = begin
+      p  ≡⟨ sym m*1=m  ⟩
+      p * 1  ≡⟨ sym m*1=m ⟩
+      p * 1 * 1   ≡⟨ cong (λ k → p * k * k ) (sym b) ⟩
+      p * j * j   ≡⟨ r00 ⟩
+      i * i  ∎ where open ≡-Reasoning
      r03 : p ≡ i * i → i > 1
-     r03 = {!!}
+     r03 eq with <-cmp i 1
+     ... | tri< a ¬b ¬c = {!!}
+     ... | tri≈ ¬a b ¬c = {!!}
+     ... | tri> ¬a ¬b c = c
+     r02 : p ≡ i * i → gcd p i ≡ i 
+     r02 eq = GCD.div→gcd (r03 r01) record { factor = i ; is-factor = trans  (+-comm _ 0 ) (sym r01) }
      r04 :  1 ≡ i
      r04 = begin
-      1 ≡⟨ {!!} ⟩
-      gcd p i   ≡⟨ {!!} ⟩
+      1 ≡⟨ sym (Prime.isPrime pr _ {!!} {!!} ) ⟩
+      gcd p i   ≡⟨ r02 r01 ⟩
       i ∎ where open ≡-Reasoning
 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1
 ... | tri< a ¬b₁ ¬c = {!!} where