# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585567324 -32400
# Node ID 908409975a5ef87d749c18e02a45009636416568
# Parent  7256d3d032e47b7f3eac40363a06e0cacafcf1a6
...

diff -r 7256d3d032e4 -r 908409975a5e prob1.agda
--- a/prob1.agda	Mon Mar 30 17:51:52 2020 +0900
+++ b/prob1.agda	Mon Mar 30 20:22:04 2020 +0900
@@ -39,6 +39,7 @@
       c1 : Cond1 A M k
       unique-i : {j : ℕ} {m1  : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.i c1 ≡ j
       unique-n : {j : ℕ} {m1  : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.n c1 ≡ m1
+      maxA : A ≤ ( k * M ) - 1
 
 problem1-0 : (k A M : ℕ )  → (A<kM : suc A <  k * M )
     → UCond1 A M k 
@@ -134,9 +135,45 @@
         unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c ))
         unique-n :  {j m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → n ≡ m1
         unique-n {j} {m1} j<M m1<k eq = unique-m (unique-i j<M m1<k eq ) (Cond1.rule1 c1) eq 
+        --   A < M + ((k - n) * M)
+        --   A < suc k * M - n * M  < suc k * M - n * M
+        lemma8 : A - ((k - n) * M) < M  → A < M + ((k - n) * M) 
+        lemma8 i<M with <-cmp (suc (suc A)) ( (k - n) * M )
+        lemma8 i<M | tri< a ¬b ¬c = {!!}
+        lemma8 i<M | tri≈ ¬a b ¬c = {!!}
+        lemma8 i<M | tri> ¬a ¬b c = begin
+                  suc A
+               ≡⟨ sym ( minus+n {suc A} {(k - n) * M} c )  ⟩
+                  (suc A - ((k - n) * M)) + (k - n) * M
+               ≡⟨ {!!}  ⟩
+                  suc ( (A - ((k - n) * M)) + ((k - n) * M) )
+               ≤⟨  ≤-plus i<M  ⟩ 
+                   M + ((k - n) * M)
+               ∎ where open ≤-Reasoning
+        lemma9 : {x y : ℕ } → suc x ≤ y → x ≤ y - 1
+        lemma9 {zero} {zero} ()
+        lemma9 {suc x} {zero} ()
+        lemma9 {x} {suc y} (s≤s lt) = lt
+        maxA : A - ((k - n) * M) < M  → A ≤ (suc k * M ) - 1
+        maxA i<M = begin
+                  A
+               ≤⟨ lemma9 (lemma8 i<M ) ⟩ 
+                  (M + ((k - n) * M)) - 1
+               ≡⟨ cong (λ k → (M + k ) - 1 ) (distr-minus-* {k} {n} {M} ) ⟩ 
+                  (M + ((k * M) - ( n * M))) - 1
+               ≡⟨ {!!} ⟩ 
+                  ((M + (k * M) )- ( n * M)) - 1
+               ≡⟨⟩ 
+                  ((suc k * M )- ( n * M)) - 1
+               ≡⟨ {!!} ⟩ 
+                  (suc k * M) - ((n * M) + 1)
+               ≤⟨ {!!}  ⟩ 
+                  (suc k * M ) - 1
+               ∎ where open ≤-Reasoning
         c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 }
             ; unique-i = unique-i 
             ; unique-n = unique-n
+            ; maxA = maxA i<M
             }
      --  loop on  range  of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M
      nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M)