# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678630632 -32400
# Node ID c19d3af3039448a211a97dec4721b3b2290b244c
# Parent  6f3636fbc481d3d430419cd090dc72bbb7dbcfc6
...

diff -r 6f3636fbc481 -r c19d3af30394 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Sun Mar 12 22:49:59 2023 +0900
+++ b/automaton-in-agda/src/nat.agda	Sun Mar 12 23:17:12 2023 +0900
@@ -282,7 +282,7 @@
 
 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
+... | tri< a ¬b ¬c = +-cancelʳ-<  (y - x) _ ( begin
          suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩
          suc y  ≡⟨ +-comm 1 _ ⟩
          y + suc 0  ≤⟨ +-mono-≤ ≤-refl 0<x ⟩
@@ -424,6 +424,13 @@
 m*1=m {zero} = refl
 m*1=m {suc m} = cong suc m*1=m
 
++-cancel-1 : (x y z : ℕ ) → x + y  ≡ x + z  → y ≡ z
++-cancel-1 zero y z eq = eq
++-cancel-1 (suc x) y z eq = +-cancel-1 x y z (cong pred eq )
+
++-cancel-0 : (x y z : ℕ ) → y + x ≡ z + x → y ≡ z
++-cancel-0 x y z eq = +-cancel-1 x y z (trans (+-comm x y) (trans eq (sym (+-comm x z)) ))
+
 *-cancel-left : {x y z : ℕ } → x > 0 → x * y ≡ x * z → y ≡ z
 *-cancel-left {suc x} {zero} {zero} lt eq = refl
 *-cancel-left {suc x} {zero} {suc z} lt eq = ⊥-elim ( nat-≡< eq (s≤s (begin
@@ -435,19 +442,19 @@
   zero  ≤⟨ z≤n ⟩ 
   _ ∎ ))) where open ≤-Reasoning
 *-cancel-left {suc x} {suc y} {suc z} lt eq with cong pred eq
-... | eq1 =  cong suc (*-cancel-left {suc x} {y} {z} lt ( proj₂ +-cancel-≡ x _ _ (begin
-  y + x * y + x ≡⟨ +-assoc y _ _ ⟩ 
-  y + (x * y + x) ≡⟨ cong (λ k → y + (k + x)) (*-comm x _)  ⟩ 
-  y + (y * x + x) ≡⟨ cong (_+_ y) (+-comm _ x) ⟩ 
-  y + (x + y * x ) ≡⟨ refl ⟩ 
-  y + suc y * x ≡⟨ cong (_+_ y) (*-comm (suc y) _)  ⟩ 
-  y + x * suc y ≡⟨ eq1 ⟩ 
-  z + x * suc z ≡⟨ refl ⟩ 
-  _ ≡⟨ sym ( cong (_+_ z) (*-comm (suc z) _) ) ⟩ 
-  _ ≡⟨ sym ( cong (_+_ z) (+-comm _ x)) ⟩ 
-  z + (z * x + x) ≡⟨ sym ( cong (λ k → z + (k + x)) (*-comm x _) ) ⟩ 
-  z + (x * z + x) ≡⟨ sym ( +-assoc z _ _) ⟩ 
-  z + x * z + x  ∎ ))) where open ≡-Reasoning
+... | eq1 =  cong suc (*-cancel-left {suc x} {y} {z} lt (+-cancel-0 x _ _ (begin
+   y + x * y + x ≡⟨ +-assoc y _ _ ⟩ 
+   y + (x * y + x) ≡⟨ cong (λ k → y + (k + x)) (*-comm x _)  ⟩ 
+   y + (y * x + x) ≡⟨ cong (_+_ y) (+-comm _ x) ⟩ 
+   y + (x + y * x ) ≡⟨ refl ⟩ 
+   y + suc y * x ≡⟨ cong (_+_ y) (*-comm (suc y) _)  ⟩ 
+   y + x * suc y ≡⟨ eq1 ⟩ 
+   z + x * suc z ≡⟨ refl ⟩ 
+   _ ≡⟨ sym ( cong (_+_ z) (*-comm (suc z) _) ) ⟩ 
+   _ ≡⟨ sym ( cong (_+_ z) (+-comm _ x)) ⟩ 
+   z + (z * x + x) ≡⟨ sym ( cong (λ k → z + (k + x)) (*-comm x _) ) ⟩ 
+   z + (x * z + x) ≡⟨ sym ( +-assoc z _ _) ⟩ 
+   z + x * z + x  ∎ ))) where open ≡-Reasoning
 
 record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set  (n Level.⊔ m) where
   field