# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624801400 -32400
# Node ID 9f7e4a4415f72575cc26913fa9d2b86f463ac5e8
# Parent  938d48130144fb46a455098e6a5f245708b88ab1
...

diff -r 938d48130144 -r 9f7e4a4415f7 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Sun Jun 27 18:49:54 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sun Jun 27 22:43:20 2021 +0900
@@ -523,17 +523,23 @@
    ea = Equlid.eqa e 
    eb = Equlid.eqb e
    f = Dividable.factor (proj1 di)
+   ge4 :  suc (j0 + 0) > suc (suc j)
+   ge4 = {!!}
    ge0 : (ea + eb * f) * suc i0 > eb * j0 → (((ea + eb * f) * suc i0) - (eb * j0)) ≡ gcd1 i0 (suc i0) (suc j) (suc (suc j))
    ge0 lt = subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Equlid.is-equ< e ge2 ) ge1 where
     ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
     ge1  = begin
-      ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ {!!}   ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm 0 _) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (j0 + 0) )  ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (sym (minus+n {j0 + 0} {suc (suc j)} {!!} )) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (((j0 + 0) -  suc (suc j)) + suc (suc j)  )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * k)) (+-comm _ (suc (suc j)) ) ⟩
       ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + ((j0 + 0) -  suc (suc j))))
               ≡⟨ cong (λ k → ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k) )) (sym (Dividable.is-factor (proj1 di)))  ⟩ 
-      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 + 0) )) ≡⟨ {!!} ⟩ 
-      ((ea + eb * f ) * suc i0) - eb * (f * (suc i0) + suc (suc j) )  ≡⟨ {!!} ⟩ 
-      (ea + eb * f ) * suc i0 - ((eb * f) * (suc i0) + eb * suc (suc j))   ≡⟨ {!!} ⟩ 
-      ((ea * suc i0 + (eb * f ) * suc i0 ) - (eb * f) * (suc i0)) + eb * suc (suc j)   ≡⟨ {!!} ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 + 0) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + k))) (+-comm _ 0) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * (suc (suc j) + (f * suc i0 ) )) ≡⟨ cong (λ k →  ((ea + eb * f ) * suc i0) - k) (*-distribˡ-+  eb (suc (suc j)) (f * suc i0)) ⟩ 
+      ((ea + eb * f ) * suc i0) - (eb * suc (suc j) + eb * (f * suc i0)) ≡⟨ cong (λ k → k - (eb * suc (suc j) + eb * (f * suc i0))) (*-distribʳ-+ (suc i0)  ea  _) ⟩ 
+      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + (eb * (f * (suc i0))) )
+           ≡⟨ cong (λ k →  (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + k )) (sym (*-assoc eb _ _ )) ⟩ 
+      (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + ((eb * f) * (suc i0)) )   ≡⟨ minus+xy-zy {ea * suc i0} {(eb * f ) * suc i0} {eb * suc (suc j)}  ⟩ 
       (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
     ge2 : ea * suc i0 > eb * suc (suc j)
     ge2 = ge3 lt ge1 
diff -r 938d48130144 -r 9f7e4a4415f7 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Sun Jun 27 18:49:54 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Sun Jun 27 22:43:20 2021 +0900
@@ -240,6 +240,13 @@
          suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩
          suc x ∎  where open ≡-Reasoning
 
+minus+yx-yz : {x y z : ℕ } → (y + x) - (y + z)  ≡ x - z
+minus+yx-yz {x} {zero} {z} = refl
+minus+yx-yz {x} {suc y} {z} = minus+yx-yz {x} {y} {z} 
+
+minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y)  ≡ x - z
+minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z  ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z})
+
 y-x<y : {x y : ℕ } → 0 < x → 0 < y  → y - x  <  y
 y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y)
 ... | tri< a ¬b ¬c = +-cancelʳ-< {x} (y - x) y ( begin