--- a/prob1.agda	Sat Mar 28 18:38:15 2020 +0900
+++ b/prob1.agda	Sun Mar 29 08:29:21 2020 +0900
@@ -169,8 +169,12 @@
      cck n n<k k<A i<M = c0 where
         c1 : Cond1 A M (suc k) 
         c1 = kk.cck k A m A<kM n n<k k<A i<M 
+        lemma2 : {i j n m1 : ℕ} → j < i  → i + suc k * M ≡ M * suc n + A → j + suc k * M ≡ M * suc m1 + A → j + suc k * M + M < suc (i + suc k * M )
+        lemma2 = {!!}
+        lemma3 : {i j : ℕ} → j + suc k * M + M < suc (i + suc k * M ) → j + M < suc i
+        lemma3 = {!!}
         lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
-        lemma-u1 = {!!}
+        lemma-u1 {j} {m1} j<akM m1<k eq = {!!}
         c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 } ; u1 = lemma-u1 }
      cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k)
      cc zero n<k k<A = cck 0 n<k k<A lemma where
@@ -181,10 +185,41 @@
      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 a
      cc (suc n) n<k k<A | tri≈ ¬a b ¬c = 
-         record { c1 = UCond1.c1 (cc n {!!} {!!}) ; u1 = {!!}  }
+        cc n (less-1 n<k) (lemma1 b)  where
+        a=mk0 :  (A - ((k - (suc n)) * M)) ≡  M → A ≡ (k - n) * M
+        a=mk0 a=mk = sym ( begin
+           (k - n) * M 
+         ≡⟨ sym ( minus+n {(k - n) * M} {M} (kk.nextc k A m A<kM n n<k )) ⟩
+           ((k - n) * M ) - M + M
+         ≡⟨ +-comm _ M ⟩
+           M + (((k - n) * M ) - M)
+         ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} (<-minus-0 n<k ))) ⟩
+           M + (k - (suc n) * M) 
+         ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩
+           A - ((k - (suc n)) * M) + ((k - (suc n)) * M) 
+         ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩
+           A
+         ∎ ) where open ≡-Reasoning
+        lemma1 : (A - ((k - (suc n)) * M)) ≡  M → suc A > (k - n) * M
+        lemma1 a=mk = subst (λ x → (k - n) * M < suc x ) (sym (a=mk0 a=mk )) a<sa
      cc (suc n) n<k k<A | tri> ¬a ¬b c = 
-         record { c1 = UCond1.c1 (cc n {!!} {!!}) ; u1 = {!!}  }
-
+        cc n (less-1 n<k) (lemma3 c) where
+        lemma3 : (A - ((k - (suc n)) * M)) > M  → suc A > (k - n) * M
+        lemma3 mk<a = <-trans lemma5 a<sa where
+            lemma6 :  M + (k - (suc n)) * M ≡ (k - n) * M
+            lemma6 = begin
+                  M + (k - (suc n)) * M 
+               ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k))  ⟩
+                  M + (((k - n) * M ) - M )
+               ≡⟨ +-comm M _ ⟩
+                  ((k - n) * M ) - M + M
+               ≡⟨ minus+n {_} {M} (kk.nextc k A m A<kM n n<k ) ⟩
+                  (k - n) * M
+               ∎  where open ≡-Reasoning
+            lemma4 : (M + (k - (suc n)) * M) < A
+            lemma4 = subst (λ x → (M + (k - (suc n)) * M)  < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a )
+            lemma5 : (k - n) * M < A
+            lemma5 = subst (λ x → x < A ) lemma6 lemma4
      start-range : (k : ℕ ) → suc A > (k - k) * M
      start-range zero = s≤s z≤n
      start-range (suc k) = start-range k