# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574683666 -32400
# Node ID e909c828cefe57c05e9b37afb6fbe727ebe84503
# Parent  0dcf08f3ff182027e2159341eef1fe9118bab9a4
which way?

diff -r 0dcf08f3ff18 -r e909c828cefe prob1.agda
--- a/prob1.agda	Mon Nov 25 21:05:25 2019 +0900
+++ b/prob1.agda	Mon Nov 25 21:07:46 2019 +0900
@@ -80,8 +80,8 @@
 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 where
-     ccn :  (suc (suc A) >  k * M )  →  Cond1 A M (suc k)
-     ccn gt =  record { n = 0 ; i = minus A (k * M ) ; range-n = s≤s z≤n ; range-i = A-Mk<M {!!} A<kM ; rule1 = lemma1 } where
+     ccn :  (suc A >  k * M )  →  Cond1 A M (suc k)
+     ccn gt =  record { n = 0 ; i = minus A (k * M ) ; range-n = s≤s z≤n ; range-i = A-Mk<M {k} gt A<kM ; rule1 = lemma1 } where
         A-Mk<M : {k A M : ℕ } → (suc A >  k * M ) → ( suc A <  (suc k ) * M ) → minus A (k * M ) < M
         A-Mk<M {k} {A} {M} lt1 lt2 = <-minus ( subst₂ (λ j k → j <  k ) (sym (minus+n {A} {k * M} lt1 )) refl (<-trans a<sa lt2) )
         lemma1 : minus A (k * M) + suc k * M ≡ M * 1 + A
@@ -93,7 +93,7 @@
               minus A (k * M) + (k * M + M )
            ≡⟨ sym ( +-assoc _ (k * M ) M ) ⟩
               (minus A (k * M) + k * M ) + M 
-           ≡⟨ cong ( λ k → k + M ) (minus+n {A} {k * M} ? ) ⟩
+           ≡⟨ cong ( λ k → k + M ) (minus+n {A} {k * M} gt ) ⟩
               A + M 
            ≡⟨⟩
               A + ( 0 + M )
@@ -112,8 +112,8 @@
      cc :  Cond1 A M (suc k)
      cc with <-cmp (suc A) (k * M)
      cc | tri< a ¬b ¬c = next-cc A M k ( problem0-k=k k A M ) a 
-     cc | tri≈ ¬a b ¬c = ccn (subst (λ x → x > k * M ) (cong (λ k → suc k) (sym b )) a<sa  )
-     cc | tri> ¬a ¬b c = ccn (<-trans c a<sa)
+     cc | tri≈ ¬a b ¬c = next-cc A M k ( problem0-k=k k A M ) ? 
+     cc | tri> ¬a ¬b c = ccn 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