# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1642176763 -32400
# Node ID 39f0e1d7a7e52a8c7f50419fca4ee82fd4acaac7
# Parent  329adb1b71c794805a5ebcf9113c53f542b117df
root2 fulcomp

diff -r 329adb1b71c7 -r 39f0e1d7a7e5 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Fri Jan 14 22:58:25 2022 +0900
+++ b/automaton-in-agda/src/root2.agda	Sat Jan 15 01:12:43 2022 +0900
@@ -189,36 +189,17 @@
       d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
       Rational.i r * Rational.i r  ∎ where open ≡-Reasoning
 
-    
+*<-2 : {x y z : ℕ} → z > 0  → x < y → z * x < z * y   
+*<-2 {x} {y} {suc z} (s≤s z>0) x<y = *-monoʳ-< z x<y
+
+r15 : {p : ℕ} → p > 1 → p < p * p
+r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )
 
 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r  : Rational ) → ¬ ( Rational* r r r= p )
 root-prime-irrational1 p pr r div  with <-cmp (Rational.j r) 1
-... | tri< a ¬b ¬c = ⊥-elim (nat-≤> (Rational.0<j r) a )
-... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< r04 (r03 r01)) 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
-     r01 : p ≡ i * i
-     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 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 ≡⟨ 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₁ = 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) )
 ... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≡< (sym r05) r08) where
      i = Rational.i r
      j = Rational.j r
@@ -229,17 +210,85 @@
      ... | tri≈ ¬a b ¬c = b
      ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c a )
      r05 : p * j * j ≡ 0 
-     r05 = {!!}
+     r05 with r06
+     ... | refl = r00
+     r09 : p * j  > 0
+     r09 = begin
+        suc zero ≤⟨ <-trans a<sa (Prime.p>1 pr)  ⟩
+        p ≡⟨ sym m*1=m ⟩
+        p * 1 <⟨ *<-2 (<-trans a<sa (Prime.p>1 pr)) c ⟩
+        p * j  ∎ where open ≤-Reasoning
      r08 : p * j * j > 0
-     r08 = {!!}
+     r08 = begin
+        suc zero ≤⟨ r09  ⟩
+        p * j ≡⟨ sym m*1=m ⟩
+        (p * j) * 1 <⟨ *<-2 r09 c ⟩
+        (p * j) * j ∎ where open ≤-Reasoning
 ... | 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 ≡ 1  
-     r07 = {!!}
+     r07 = begin
+        p * j * j ≡⟨ r00 ⟩
+        i * i  ≡⟨ cong (λ k → k * k) b ⟩
+        1 * 1 ≡⟨⟩
+        1 ∎ where open ≡-Reasoning
+     r19 : 1 < p * j  
+     r19 = begin 
+        suc 1 ≤⟨ Prime.p>1 pr ⟩
+        p ≡⟨ sym m*1=m ⟩
+        p * 1 <⟨  *<-2 (<-trans a<sa (Prime.p>1 pr)) c ⟩
+        p * j ∎ where open ≤-Reasoning
      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) )
+     r09 = begin 
+        suc 1 ≤⟨ r19  ⟩
+        p * j ≡⟨ sym  m*1=m ⟩
+        p * j * 1 <⟨  *<-2  (<-trans a<sa r19 )  c ⟩
+        (p * j) * j ∎ where open ≤-Reasoning
+root-prime-irrational1 p pr r div | tri< a ¬b ¬c = ⊥-elim (nat-≤> (Rational.0<j r) a )
+root-prime-irrational1 p pr r div | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< r04 (r03 r01)) where
+     i = Rational.i r
+     j = Rational.j r
+     p>0 : p > 0
+     p>0 = <-trans a<sa (Prime.p>1 pr)
+     r00 : p * j * j ≡ i * i
+     r00 = r3 p p>0 r div
+     r01 : p ≡ i * i
+     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 eq with <-cmp i 1
+     ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym r11) p>0 ) where
+          r10 : i ≡ 0
+          r10 with <-cmp i 0
+          ... | tri≈ ¬a b ¬c = b
+          ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c a )
+          r11 : p ≡ 0
+          r11 = begin
+             p   ≡⟨ r01 ⟩
+             i * i   ≡⟨ cong (λ k → k * k ) r10 ⟩
+             0 * 0   ≡⟨⟩
+             0  ∎ where open ≡-Reasoning
+     ... | tri≈ ¬a refl ¬c = ⊥-elim (  nat-≡< (sym r01 ) (Prime.p>1 pr)) 
+     ... | 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) }
+     r14 : i < p 
+     r14 with <-cmp i p
+     ... | tri< a ¬b ¬c = a
+     ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< r01 (begin
+             suc p ≤⟨ r15 (Prime.p>1 pr) ⟩
+             p * p  ≡⟨ cong (λ k → k * k ) (sym b) ⟩
+             i * i ∎ )) where open ≤-Reasoning
+     ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< r01 (<-trans c (r15 (r03 r01 )))) 
+     r04 :  1 ≡ i
+     r04 = begin
+        1 ≡⟨ sym (Prime.isPrime pr _ r14 (<-trans a<sa (r03 r01 ))) ⟩
+        gcd p i   ≡⟨ r02 r01 ⟩
+        i ∎ where open ≡-Reasoning