# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585492578 -32400
# Node ID f2db03a8af2c2d8dd895aedbca35a530c5929008
# Parent  c5ed490494bc4d38767bda234ef19babd161bfa6
...

diff -r c5ed490494bc -r f2db03a8af2c prob1.agda
--- a/prob1.agda	Sun Mar 29 08:29:21 2020 +0900
+++ b/prob1.agda	Sun Mar 29 23:36:18 2020 +0900
@@ -174,7 +174,11 @@
         lemma3 : {i j : ℕ} → j + suc k * M + M < suc (i + suc k * M ) → j + M < suc i
         lemma3 = {!!}
         lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
-        lemma-u1 {j} {m1} j<akM m1<k eq = {!!}
+        lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M
+        lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c = {!!}
+        lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) 
+            -- (suc (minus A (minus k n * suc m))) !=< (minus A (minus k n * suc m))
+        lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) 
         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 }
      cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k)
      cc zero n<k k<A = cck 0 n<k k<A lemma where