--- a/nat.agda	Sun Mar 29 23:36:18 2020 +0900
+++ b/nat.agda	Mon Mar 30 02:10:49 2020 +0900
@@ -142,6 +142,18 @@
 x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
 x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
 
+≤-minus-0 : {x y z : ℕ } → z + x ≤ z + y → x ≤ y
+≤-minus-0 {x} {y} {zero} lt = lt
+≤-minus-0 {x} {y} {suc z} (s≤s lt) = ≤-minus-0 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 )
+
+x+y≤z→x≤z : {x y z : ℕ } → x + y ≤ z → x ≤ z 
+x+y≤z→x≤z {zero} z≤n = z≤n
+x+y≤z→x≤z {zero} (s≤s lt) = z≤n
+x+y≤z→x≤z {suc x} (s≤s lt) = s≤s ( x+y≤z→x≤z lt )
+
 *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
 *≤ lt = *-mono-≤ lt ≤-refl
 

--- a/prob1.agda	Sun Mar 29 23:36:18 2020 +0900
+++ b/prob1.agda	Mon Mar 30 02:10:49 2020 +0900
@@ -169,15 +169,29 @@
      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 = {!!}
+        lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z
+        lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y)
+        lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) )
+        lemma5 : {m1  : ℕ} →      M * suc m1 + A  < M * suc n + A
+                           → M + (M * suc m1 + A) ≤ M * suc n + A  
+        lemma5 = {!!}
+        lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i
+        lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin 
+                 M + x + j 
+               ≡⟨ +-assoc M _ _ ⟩
+                 M + (x + j )
+               ≡⟨ cong (λ k → M + k  ) (+-comm x _ ) ⟩
+                 M + (j + x)
+               ≤⟨ lt  ⟩
+                 i + x 
+               ∎ )) where open ≤-Reasoning
         lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
         lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M
-        lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c = {!!}
+        lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c =
+            ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) (lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM ))) ) i<M ) where
+             lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A
+             lemma3 = lemma5 (lemma4  eq (Cond1.rule1 c1) j<akM)
         lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) 
-            -- (suc (minus A (minus k n * suc m))) !=< (minus A (minus k n * suc m))
         lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) 
         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)