--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 12:29:04 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 14:57:40 2021 +0900
@@ -564,9 +564,9 @@
 
 gcd-euclid1 : ( i i0 j j0 : ℕ )  → GCD i i0 j j0  → Euclid i0 j0 (gcd1 i i0 j j0)
 gcd-euclid1 zero i0 zero j0 di with <-cmp i0 j0
-... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = {!!} ; is-equ> = {!!}  }
-... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = {!!} ; is-equ> = {!!} } 
-... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ;  is-equ< = {!!} ; is-equ> = {!!} }
+... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () }
+... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () } 
+... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ;  is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 }
 gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
 gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
 gcd-euclid1 zero (suc i0) (suc (suc j)) j0 di with gcd-euclid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
@@ -594,11 +594,17 @@
       ;  is-equ> =  λ lt → subst (λ k →  (((eb + ea * f) * suc j0) - (ea * i0)) ≡ k ) (Euclid.is-equ> e (ge3 lt ge5)) ge5 } where
    ea = Euclid.eqa e 
    eb = Euclid.eqb e
-   f = Dividable.factor (GCD.div-i di)
+   f = Dividable.factor (GCD.div-j di)
    ge5 : (((eb + ea * f) * suc j0) - (ea * i0)) ≡ ((eb * suc j0) - (ea * suc (suc i)))
-   ge5 = {!!}
+   ge5 = begin
+       ((eb + ea * f) * suc j0) - (ea * i0) ≡⟨ cong₂ (λ j k → j - k ) (proj1 (ge01 j0 i i0 eb ea (GCD-sym di) )) (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )) ⟩
+      ( eb * suc j0 + (ea * f )* suc j0) - (ea * suc (suc i) + (ea * f )* suc j0) ≡⟨ minus+xy-zy {_} {(ea * f )* suc j0} {ea * suc (suc i)}   ⟩
+       (eb * suc j0) - (ea * suc (suc i)) ∎ where open ≡-Reasoning
    ge4 : ((ea * i0) - ((eb + ea * f) * suc j0)) ≡ ((ea * suc (suc i)) - (eb * suc j0))
-   ge4 = {!!}
+   ge4 = begin
+        (ea * i0) - ((eb + ea * f) * suc j0) ≡⟨ cong₂ (λ j k → j - k ) (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )) (proj1 (ge01 j0 i i0 eb ea (GCD-sym di) )) ⟩
+        (ea * suc (suc i) + (ea * f )* suc j0) - ( eb * suc j0 + (ea * f )* suc j0)  ≡⟨ minus+xy-zy {ea * suc (suc i)} {(ea * f )* suc j0} { eb * suc j0}   ⟩
+        (ea * suc (suc i)) - (eb * suc j0) ∎ where open ≡-Reasoning
 gcd-euclid1 (suc zero) i0 (suc j) j0 di =
      gcd-euclid1 zero i0 j j0  (gcd-next di)
 gcd-euclid1 (suc (suc i)) i0 (suc j) j0  di =