# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574844719 -32400
# Node ID 3557795c7bb3ecc9dd9842504b80ef6523ebb1d2
# Parent  559bada080d59cc30586ebd7bb7f712ecd50b7ed
problem 0 done

diff -r 559bada080d5 -r 3557795c7bb3 nat.agda
--- a/nat.agda	Wed Nov 27 13:47:04 2019 +0900
+++ b/nat.agda	Wed Nov 27 17:51:59 2019 +0900
@@ -129,12 +129,14 @@
 <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y 
 <-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )
 
-≤-plus-≡ : {x y z : ℕ } → (x ≤ y ) ≡ (z + x ≤ z + y )
-≤-plus-≡ {zero} {zero} {zero} = refl
-≤-plus-≡ {zero} {zero} {suc z} with ≤-plus-≡ {zero} {zero} {z}
-... | eq = {!!}
-≤-plus-≡ {zero} {suc y} {z} = {!!}
-≤-plus-≡ {suc x} {y} {z} = {!!}
+≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
+≤-plus {0} {y} {zero} z≤n = z≤n
+≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y 
+≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )
+
+≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y 
+≤-plus-0 {x} {y} {zero} lt = lt
+≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )
 
 x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z 
 x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
@@ -245,10 +247,22 @@
              lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y}  lemma1 ))  gt )
 
 minus-* : {M k n : ℕ } → n < k  → minus k (suc n) * M ≡ minus (minus k n * M ) M
-minus-* {zero} {k} {n} lt = {!!}
+minus-* {zero} {k} {n} lt = begin
+           minus k (suc n) * zero
+        ≡⟨ *-comm (minus k (suc n)) zero ⟩
+           zero * minus k (suc n) 
+        ≡⟨⟩
+           0 * minus k n 
+        ≡⟨ *-comm 0 (minus k n) ⟩
+           minus (minus k n * 0 ) 0
+        ∎  where
+        open ≡-Reasoning
 minus-* {suc m} {k} {n} lt with <-cmp k 1
-minus-* {suc m} {k} {n} lt | tri< a ¬b ¬c = {!!}
-minus-* {suc m} {k} {n} lt | tri≈ ¬a b ¬c = {!!}
+minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
+minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
+minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
+minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt 
+minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
 minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
            minus k (suc n) * M
         ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
@@ -262,18 +276,14 @@
         ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
            minus (minus k n * M ) M
         ∎  where
-             open ≡-Reasoning
              M = suc m
              lemma : {n k m : ℕ } → n < k  → suc (k * suc m) > suc m + n * suc m
              lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
-             lemma {suc n} {suc k} {m} (s≤s lt) = lemma1 (lemma {n} {k} {m} lt ) where
-                 lemma1 : suc (suc m + n * suc m) ≤ suc (k * suc m) → suc (suc m + suc n * suc m ) ≤ suc (suc k * suc m) 
-                 lemma1 (s≤s lt) = s≤s ( s≤s (subst (λ x → x ) (
-                   begin
-                     suc m + n * suc m ≤ k * suc m
-                   ≡⟨⟩
-                     suc n * suc m     ≤ k * suc m
-                   ≡⟨ ≤-plus-≡ ⟩
-                     m + suc n * suc m ≤ m + k * suc m
-                   ∎ ) lt ))  where open ≡-Reasoning
-
+             lemma {suc n} {suc k} {m} lt = begin
+                         suc (suc m + suc n * suc m) 
+                      ≡⟨⟩
+                         suc ( suc (suc n) * suc m)
+                      ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
+                         suc (suc k * suc m)
+                      ∎   where open ≤-Reasoning
+             open ≡-Reasoning