# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1623893100 -32400
# Node ID 875b811f3ff1ec63de720475a10bf9baf0b35c80
# Parent  b5e8e6be9425e94bf188266351a7682e20096de9
...

diff -r b5e8e6be9425 -r 875b811f3ff1 logic.agda
--- a/logic.agda	Tue Mar 31 01:43:50 2020 +0900
+++ b/logic.agda	Thu Jun 17 10:25:00 2021 +0900
@@ -2,7 +2,7 @@
 
 open import Level
 open import Relation.Nullary
-open import Relation.Binary
+open import Relation.Binary hiding ( _⇔_ )
 open import Data.Empty
 
 
diff -r b5e8e6be9425 -r 875b811f3ff1 nat.agda
--- a/nat.agda	Tue Mar 31 01:43:50 2020 +0900
+++ b/nat.agda	Thu Jun 17 10:25:00 2021 +0900
@@ -8,7 +8,7 @@
 open import  Relation.Binary.PropositionalEquality
 open import  Relation.Binary.Core
 open import  logic
--- open import Relation.Binary.Definitions
+open import Relation.Binary.Definitions
 
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
@@ -181,9 +181,9 @@
 <tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
 <tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)
 
-≤to< : {x y  : ℕ } → x < y → x ≤ y 
-≤to< {zero} {suc y} (s≤s z≤n) = z≤n
-≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y}  lt)
+<to≤ : {x y  : ℕ } → x < y → x ≤ y 
+<to≤ {zero} {suc y} (s≤s z≤n) = z≤n
+<to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y}  lt)
 
 refl-≤s : {x : ℕ } → x ≤ suc x
 refl-≤s {zero} = z≤n
@@ -281,7 +281,7 @@
             le : x * z ≤ z + y * z
             le  = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
                lemma : x * z ≤ y * z
-               lemma = *≤ {x} {y} {z} (≤to< a)
+               lemma = *≤ {x} {y} {z} (<to≤ a)
 distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
           minus x (suc y) * z
         ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
diff -r b5e8e6be9425 -r 875b811f3ff1 prob1.agda
--- a/prob1.agda	Tue Mar 31 01:43:50 2020 +0900
+++ b/prob1.agda	Thu Jun 17 10:25:00 2021 +0900
@@ -73,7 +73,7 @@
         lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y)
         lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) )
         lemma5 : {m1 n : ℕ} →      M * suc m1 + A  < M * suc n + A
-                           → M + (M * suc m1 + A) ≤ M * suc n + A  
+                            → M + (M * suc m1 + A) ≤ M * suc n + A  
         lemma5 {m1} {n} lt with <-cmp m1 n
         lemma5 {m1} {n} lt | tri< a ¬b ¬c = begin
                    M + (M * suc m1 + A)
@@ -119,6 +119,7 @@
         unique-i {j} {m1} j<M m1<k eq | tri< a ¬b ¬c = ⊥-elim ( lemma-u2 a j<M m1<k eq  )
         unique-i {j} {m1} j<M m1<k eq | tri≈ ¬a b ¬c = b
         unique-i {j} {m1} j<M m1<k eq | tri> ¬a ¬b c = ⊥-elim ( lemma-u1 c m1<k eq  )
+
         lemma7 : {n m1 m A  : ℕ} → n < m1   → suc (n + m * suc n + A) < suc (m1 + m * suc m1 + A)
         lemma7 {n} {m1} {m} {A} n<m1 = begin
                   suc (suc (n + m * suc n + A))
@@ -160,7 +161,7 @@
         lemma8 : A - ((k - n) * M) < M  → A < M + ((k - n) * M) 
         lemma8 i<M with <-cmp (suc A) ( (k - n) * M )
         lemma8 i<M | tri< a ¬b ¬c = <-minus-0 {A} {_} {suc zero} ( <-trans a (<to<s lemmab) ) 
-        lemma8 i<M | tri≈ ¬a b ¬c = <-minus-0 {A} {_} {suc zero} (subst (λ h → h < 1 + suc (m + minus k n * suc m)) (sym b) (<to<s lemmab)) where
+        lemma8 i<M | tri≈ ¬a b ¬c = <-minus-0 {A} {_} {suc zero} (subst (λ h → h < 1 + suc (m + minus k n * suc m)) (sym b) (<to<s lemmab)) 
         lemma8 i<M | tri> ¬a ¬b c = begin
                   suc A
                ≡⟨ sym ( minus+n {suc A} {(k - n) * M} (<-trans c a<sa) )  ⟩