# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574725016 -32400
# Node ID f5828d8af20c62a956da97943db54fc4afac2623
# Parent  fce6cadae300213482b8fc620247200e3e5ff962
...

diff -r fce6cadae300 -r f5828d8af20c prob1.agda
--- a/prob1.agda	Tue Nov 26 02:34:34 2019 +0900
+++ b/prob1.agda	Tue Nov 26 08:36:56 2019 +0900
@@ -103,14 +103,18 @@
            A + M * (suc n)                                         ≡⟨ +-comm A _ ⟩
            M * (suc n) + A
           ∎  where open ≡-Reasoning
-     i<range : {n : ℕ  } → A < (suc n) * M → minus A (minus k n * M) < M
+     i<range : {n : ℕ  } → suc A < suc ((suc n) * M) → minus A (minus k n * M) < M
      i<range = {!!}
-     cc : ( n : ℕ ) → n < suc k  → suc A < (suc k)  * M  →  Cond1 A M (suc k)
-     cc 0 n<k lt = cck 0 n<k {!!}  (i<range {!!}) 
+     gt : {n : ℕ  } → suc A < suc ((suc n) * M) →  (minus k n ) * M < suc A 
+     gt = {!!}
+     next-lt : (n : ℕ ) → suc A < (suc n)  * M  → (A > (pred n * M)) → suc A < n  * M  
+     next-lt n lt = {!!}
+     cc : ( n : ℕ ) → n < suc k  → suc A < (suc n)  * M  →  Cond1 A M (suc k)
+     cc 0 n<k lt = cck 0 n<k (gt {!!} ) (i<range {!!})
      cc (suc n) n<k lt with <-cmp A (n * M)
-     cc (suc n ) n<k lt | tri< a ¬b ¬c = cck (suc n) n<k {!!} {!!}
-     cc (suc n ) n<k lt | tri≈ ¬a b ¬c = cck (suc n) n<k {!!} {!!}
-     cc (suc n ) n<k lt | tri> ¬a ¬b c = cc n (less-1 n<k ) {!!}
+     cc (suc n ) n<k lt | tri< a ¬b ¬c = cck (suc n) n<k (gt {!!} ) (i<range {!!}) 
+     cc (suc n ) n<k lt | tri≈ ¬a b ¬c = cck (suc n) n<k (gt {!!} ) (i<range {!!}) 
+     cc (suc n ) n<k lt | tri> ¬a ¬b c = cc n (less-1 n<k ) (next-lt (suc n) lt c )
 
 problem0 : ( A M k : ℕ ) → M > 0 → k > 0 → (suc A <  k * M ) → Cond1 A M k
 problem0 A (suc M) (suc k) 0<M 0<k A<kM = lemma1 k M A<kM a<sa a<sa where