--- a/prob1.agda	Wed Nov 27 17:51:59 2019 +0900
+++ b/prob1.agda	Wed Nov 27 18:44:28 2019 +0900
@@ -32,7 +32,6 @@
 
 --   k = 1 → n = 0 →  ∀ M → A = i
 --   k = 2 → n = 1 →
-
 --   i + 2 * M = M * (suc n) + A    i = suc n → A = 0 
 
 problem : ( A M k : ℕ ) → Set 
@@ -145,6 +144,33 @@
 --          cannot1 :  { n k M i A : ℕ } → n < suc k → i < suc M →  (i + suc k * suc M ) > (  suc M * suc n + A)  → ¬ ( suc A <  suc k * suc M )
 --          cannot1 = {!!}
 
+--      range-n : n < k
+--      range-i : i < M
+--      rule1 : i + k * M  ≡ M * (suc n) + A    -- A ≡ (i + k * M ) - (M * (suc n)) 
+
+problem1-0 : (A M k : ℕ ) 
+    → (c1 : Cond1 A M k ) → (c2 : Cond1 A M k )
+    →  (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 )
+problem1-0 A (suc m) (suc k) c1 c2 = cc k a<sa (start-range k) where
+     M = suc m
+     cck :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M →  (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 ) 
+     cck n n<k k<A i<M = {!!} where
+        c0  =  record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = {!!} ; rule1 = {!!} }  
+        lemma-i :  (i : ℕ ) →  i < M  →  i + suc k * M ≡ M * suc n + A → i ≡  A - (k - n) * M
+        lemma-i = {!!}
+        lemma-n :  (n1 : ℕ ) → ¬ ( n1 ≡ n ) → ¬ ( ( i : ℕ ) → i < M  →  i + suc k * M ≡ M * suc n1 + A → i ≡  A - (k - n1) * M )
+        lemma-n = {!!}
+     cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 )
+     cc zero n<k k<A = cck 0 n<k k<A {!!}
+     cc (suc n) n<k k<A with <-cmp (A - ((k - (suc n)) * M))  M
+     cc (suc n) n<k k<A | tri< a ¬b ¬c = cck (suc n) n<k k<A {!!}
+     cc (suc n) n<k k<A | tri≈ ¬a b ¬c = {!!}
+     cc (suc n) n<k k<A | tri> ¬a ¬b c = {!!}
+
+     start-range : (k : ℕ ) → suc A > (k - k) * M
+     start-range zero = s≤s z≤n
+     start-range (suc k) = start-range k
+
 problem1 : (A1 A2 M k : ℕ ) 
     → (c1 : Cond1 A1 M k ) → (c2 : Cond1 A2 M k )
     → ( A1 ≡ A2 ) → (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 )