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

diff -r 7f806a28a866 -r 329adb1b71c7 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Fri Jan 14 22:39:40 2022 +0900
+++ b/automaton-in-agda/src/root2.agda	Fri Jan 14 22:58:25 2022 +0900
@@ -219,21 +219,27 @@
       gcd p i   ≡⟨ r02 r01 ⟩
       i ∎ where open ≡-Reasoning
 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1
-... | tri< a ¬b₁ ¬c = {!!} where
+... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≡< (sym r05) r08) where
      i = Rational.i r
      j = Rational.j r
      r00 : p * j * j ≡ i * i
      r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
      r06 : i ≡ 0
-     r06 = {!!}
-     r05 : p * j * j ≡ i * i  -- j > 0 → p * j * j > 0
+     r06 with <-cmp i 0
+     ... | tri≈ ¬a b ¬c = b
+     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c a )
+     r05 : p * j * j ≡ 0 
      r05 = {!!}
-... | tri≈ ¬a₁ b ¬c = {!!} where
+     r08 : p * j * j > 0
+     r08 = {!!}
+... | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym r07) r09) where
      i = Rational.i r
      j = Rational.j r
      r00 : p * j * j ≡ i * i
      r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
-     r07 : p * j * j ≡ i * i  -- j > 0 → p * j * j > 0
+     r07 : p * j * j ≡ 1  
      r07 = {!!}
+     r09 : 1 < p * j * j 
+     r09 = {!!}
 ... | tri> ¬a₁ ¬b₁ c₁ = root-prime-irrational (Rational.j r) (Rational.i r) p c pr c₁ (r3 p (<-trans a<sa (Prime.p>1 pr ) ) r div)
     (trans (GCD.gcdsym {Rational.j r} {_} ) (Rational.coprime r) )