# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585555381 -32400
# Node ID 8ef3eecd159f7dc33aac987a1e5d498ae7421fc4
# Parent  73511e7ddf5cea09c054053fc6d096dc632ac723
all done

diff -r 73511e7ddf5c -r 8ef3eecd159f nat.agda
--- a/nat.agda	Mon Mar 30 14:28:14 2020 +0900
+++ b/nat.agda	Mon Mar 30 17:03:01 2020 +0900
@@ -163,10 +163,16 @@
 *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
 *≤ lt = *-mono-≤ lt ≤-refl
 
+≤* : {x y z : ℕ } → x ≤ y → z * x ≤ z * y 
+≤* {x} {y} {z} lt = subst₂ (λ x y → x ≤ y ) (*-comm _ z)  (*-comm _ z) (*≤ lt)
+
 *< : {x y z : ℕ } → x < y → x * suc z < y * suc z 
 *< {zero} {suc y} lt = s≤s z≤n
 *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
 
+<* : {x y z : ℕ } → x < y → suc z * x <  suc z * y
+<* {x} {y} {z} lt =  subst₂ (λ x y → x < y ) (*-comm x _ ) (*-comm y (suc z)) (*< lt)
+
 <to<s : {x y  : ℕ } → x < y → x < suc y
 <to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
 <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
diff -r 73511e7ddf5c -r 8ef3eecd159f prob1.agda
--- a/prob1.agda	Mon Mar 30 14:28:14 2020 +0900
+++ b/prob1.agda	Mon Mar 30 17:03:01 2020 +0900
@@ -39,8 +39,8 @@
       c1 : Cond1 A M k
       u1 : {j m : ℕ} → j < Cond1.i c1  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
       u2 : {j m : ℕ} → Cond1.i c1  < j → j < M  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
-      -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1  → ¬ ( j + k * M  ≡ M * (suc m) + A    )
-      -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
+      u3 : {j m : ℕ} → j < M → m < Cond1.n c1  → ¬ ( j + k * M  ≡ M * (suc m) + A    )
+      u4 : {j m : ℕ} → j < M → Cond1.n c1 < m  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
 
 problem1-0 : (k A M : ℕ )  → (A<kM : suc A <  k * M )
     → UCond1 A M k 
@@ -112,9 +112,39 @@
         lemma-u2 {j} {m1} i<j j<M m1<k eq = ⊥-elim ( nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym (Cond1.rule1 c1)) (sym eq) lemma3-2)) j<M ) where
              lemma3-2 : M + (M * suc n + A) ≤ M * suc m1 + A -- M + i ≤ j
              lemma3-2 = lemma5 (lemma4 (Cond1.rule1 c1) eq i<j)
+        unique-i : {j : ℕ} {m1  : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → i ≡ j
+        unique-i {j} {m1} j<M m1<k eq with <-cmp i j
+        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))
+               ≡⟨ +-assoc _ (m * suc n)  A ⟩
+                  suc (suc n + (m * suc n + A))
+               ≤⟨ s≤s (<-plus n<m1) ⟩
+                  suc (m1 + (m * suc n + A))
+               ≡⟨ sym ( +-assoc _ (m * suc n)  A) ⟩
+                  suc (m1 + m * suc n + A)
+               ≤⟨ ≤-plus {_} {_} {A} (≤-plus-0 {_} {_} {suc m1} (≤* {suc n} {suc m1} {m} (s≤s (≤to< n<m1 )))) ⟩ 
+                  suc (m1 + m * suc m1 + A)
+               ∎ where open ≤-Reasoning
+        unique-m : {i j : ℕ} {n m1  : ℕ}  → i ≡ j → i + suc k * M ≡ M * suc n + A → j + suc k * M ≡ M * suc m1 + A → n ≡ m1
+        unique-m {i} {_} {n} {m1} refl eqn eqm with <-cmp n m1
+        unique-m {i} {_} {n} {m1} refl eqn eqm | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym (trans (sym eqm) eqn )) (lemma7 {n} {m1} {m} {A} a ))
+        unique-m {i} {_} {n} {m1} refl eqn eqm | tri≈ ¬a b ¬c = b
+        unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c ))
+        m1<sk : {m1 : ℕ} → m1 < n → n < suc k  → m1 < suc k
+        m1<sk {m1} m1<n n<k = <-trans m1<n n<k
+        lemma-u3 : {j : ℕ} {m₁ : ℕ} → j < M → m₁ < n → ¬ j + suc k * M ≡ M * suc m₁ + A
+        lemma-u3 {j} {m1} j<M m1<n eq = nat-≡< (unique-m (sym (unique-i j<M (m1<sk m1<n (Cond1.range-n c1) ) eq)) eq (Cond1.rule1 c1)) m1<n
+        lemma-u4 : {j : ℕ} {m₁ : ℕ} → j < M → n < m₁ →  m₁ < suc k  → ¬ j + suc k * M ≡ M * suc m₁ + A
+        lemma-u4 {j} {m1} j<M n<m1 m<sk eq = nat-≡< (unique-m (unique-i j<M m<sk eq) (Cond1.rule1 c1) eq ) n<m1
         c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 }
             ; u1 = lemma-u1 
             ; u2 = lemma-u2
+            ; u3 = lemma-u3
+            ; u4 = lemma-u4
             }
      --  loop on  range  of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M
      nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M)