# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574690882 -32400
# Node ID 2a36d771d38845f291a0076e127ba8d8216fb08b
# Parent  e909c828cefe57c05e9b37afb6fbe727ebe84503
add cck

diff -r e909c828cefe -r 2a36d771d388 prob1.agda
--- a/prob1.agda	Mon Nov 25 21:07:46 2019 +0900
+++ b/prob1.agda	Mon Nov 25 23:08:02 2019 +0900
@@ -25,6 +25,10 @@
 less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
 less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
 
+sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
+sa=b→a<b {0} {suc zero} refl = s≤s z≤n
+sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)
+
 minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
 minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
 minus+n {zero} {suc y} (s≤s ())
@@ -44,11 +48,13 @@
            suc x
         ∎  where open ≡-Reasoning
 
-<-minus : {x y z : ℕ } → x + z < y + z → x < y
-<-minus = {!!}
+<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
+<-minus-0 {x} {suc _} {zero} lt = lt
+<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
 
+<-minus : {x y z : ℕ } → x + z < y + z → x < y
+<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )
 
--- trans (sym (+-comm (suc y) _ )) (cong ( λ k → suc k ) {!!} ) -- (trans ? (+-comm _  _ ) )
 
 -- All variables are positive integer
 -- A = -M*n + i +k*M  - M
@@ -79,7 +85,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
+problem0-k=k (suc k) A M A<kM = cc k {!!} 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
@@ -106,14 +113,15 @@
            ≡⟨ +-comm A _ ⟩
               M * 1 + A
            ∎  where open ≡-Reasoning
+     cck :  ( n : ℕ ) →  n < k  → (suc A >  (minus k n ) * M )  →  Cond1 A M (suc k)
+     cck n n<k gt =  record { n = n ; i = minus A ((minus k n) * M ) ; range-n = {!!} ; range-i = {!!} ; rule1 = {!!} } 
 
-     next-cc : (A M k : ℕ ) → ((suc A <  k * M ) → Cond1 A M k) → (suc A <  k * M )  → Cond1 A M (suc k)
-     next-cc A M k cc A<kM = record { n = k ; i = Cond1.i (cc A<kM )  ; range-n = {!!} ; range-i = Cond1.range-i (cc A<kM ) ; rule1 = {!!} }
-     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 = next-cc A M k ( problem0-k=k k A M ) ? 
-     cc | tri> ¬a ¬b c = ccn c
+     cc : ( n : ℕ ) → (suc A >  (minus k n ) * M)  →  Cond1 A M (suc k)
+     cc 0 lt = {!!}
+     cc (suc n)  lt with <-cmp A ((minus k (suc n) ) * M)
+     cc (suc n ) lt | tri< a ¬b ¬c = cck (suc n) {!!} {!!} 
+     cc (suc n ) lt | tri≈ ¬a b ¬c = cck (suc n) {!!} {!!} 
+     cc (suc n ) lt | tri> ¬a ¬b c = cc n {!!}
 
 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