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

diff -r 310a70c03166 -r fce6cadae300 prob1.agda
--- a/prob1.agda	Tue Nov 26 02:08:50 2019 +0900
+++ b/prob1.agda	Tue Nov 26 02:34:34 2019 +0900
@@ -87,12 +87,12 @@
 
 problem0-k=k : ( k A M : ℕ ) → problem A M k
 problem0-k=k zero A M ()
-problem0-k=k (suc k) A M A<kM = cc k where
-     cck :  ( n : ℕ ) →  n < k  → (suc A >  (minus k n ) * M )  → minus A (minus k n * M) < M →  Cond1 A M (suc k)
-     cck n n<k gt lt =  record { n = n ; i = minus A ((minus k n) * M ) ; range-n = <-trans n<k a<sa  ; range-i = lt ; rule1 = lemma2 }  where
+problem0-k=k (suc k) A M A<kM = cc k a<sa A<kM where
+     cck :  ( n : ℕ ) →  n < suc k  → (suc A >  (minus k n ) * M )  → minus A (minus k n * M) < M →  Cond1 A M (suc k)
+     cck n n<k gt lt =  record { n = n ; i = minus A ((minus k n) * M ) ; range-n = n<k   ; range-i = lt ; rule1 = lemma2 }  where
         lemma2 :   minus A (minus k n * M) + suc k * M ≡ M * suc n + A
         lemma2 = begin
-           minus A (minus k n * M) + suc k * M                 ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (sym (minus+n {k} {n} (<-trans n<k a<sa ) )) ⟩
+           minus A (minus k n * M) + suc k * M                 ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩
            minus A (minus k n * M) + (suc ((minus k n ) + n )) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (+-comm _ n) ⟩
            minus A (minus k n * M) + (suc (n + (minus k n ) )) * M ≡⟨⟩
            minus A (minus k n * M) + (suc n + (minus k n ) ) * M   ≡⟨ cong ( λ x → minus A (minus k n * M) + x * M ) (+-comm (suc n) _) ⟩
@@ -103,13 +103,14 @@
            A + M * (suc n)                                         ≡⟨ +-comm A _ ⟩
            M * (suc n) + A
           ∎  where open ≡-Reasoning
-
-     cc : ( n : ℕ ) →  Cond1 A M (suc k)
-     cc 0 = cck 0 ?  ? ? 
-     cc (suc n) with <-cmp A ((minus k (suc n) ) * M)
-     cc (suc n ) | tri< a ¬b ¬c = cck (suc n) {!!} {!!} {!!}
-     cc (suc n ) | tri≈ ¬a b ¬c = cck (suc n) {!!} {!!} {!!}
-     cc (suc n ) | tri> ¬a ¬b c = cc n
+     i<range : {n : ℕ  } → A < (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 {!!}) 
+     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 ) {!!}
 
 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