# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624876132 -32400
# Node ID 6cd80d8432ead8ee0d76dd240dc91737dfb1386d
# Parent  186b66d56ab53d736582965eb7f6e508ded1381d
...

diff -r 186b66d56ab5 -r 6cd80d8432ea automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 19:11:08 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 19:28:52 2021 +0900
@@ -681,9 +681,9 @@
         ge13 : gcd p (gcd p x) ≡ gcd p x
         ge13 = {!!}
     ge10 : gcd p a ≡ 1
-    ge10 with ge12 a {!!}
+    ge10 with ge12 a 0<a
     ... | case1 x = x
-    ... | case2 x = {!!}
+    ... | case2 x = ⊥-elim ( np x )
     ge11 : Euclid p a (gcd p a)
     ge11 = gcd-euclid1 p p a a GCDi
     ge14 : ( Euclid.eqa ge11 * p ) ≤ (  Euclid.eqb ge11 * a ) → (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p + 0 ≡ b
@@ -707,11 +707,13 @@
          b ∎ where open ≡-Reasoning
     ge15 : ( Euclid.eqa ge11 * p ) > (  Euclid.eqb ge11 * a ) →  (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11  ) * p + 0 ≡ b
     ge15 = {!!}
+    ge17 : (x  y : ℕ ) → x ≡ y → x ≤ y
+    ge17 x x refl = refl-≤
     ge16 : Dividable p b
     ge16 with <-cmp ( Euclid.eqa ge11 * p ) (  Euclid.eqb ge11 * a )
-    ... | tri< a ¬b ¬c = record { factor = b * Euclid.eqa ge11 -  Dividable.factor div-ab * Euclid.eqb ge11 ; is-factor = ge14 {!!} }  
-    ... | tri≈ ¬a eq ¬c = record { factor = b * Euclid.eqa ge11 -  Dividable.factor div-ab * Euclid.eqb ge11 ; is-factor = ge14 {!!} }  
-    ... | tri> ¬a ¬b c = record { factor = Dividable.factor div-ab * Euclid.eqb ge11  - b * Euclid.eqa ge11 ; is-factor = ge15 {!!} }  
+    ... | tri< a ¬b ¬c = record { factor = b * Euclid.eqa ge11 -  Dividable.factor div-ab * Euclid.eqb ge11 ; is-factor = ge14 (<to≤ a) }  
+    ... | tri≈ ¬a eq ¬c = record { factor = b * Euclid.eqa ge11 -  Dividable.factor div-ab * Euclid.eqb ge11 ; is-factor = ge14 (ge17 _ _ eq)  }  
+    ... | tri> ¬a ¬b c = record { factor = Dividable.factor div-ab * Euclid.eqb ge11  - b * Euclid.eqa ge11 ; is-factor = ge15 c }  
 
 
 div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k