--- a/prob1.agda	Tue Nov 26 14:44:34 2019 +0900
+++ b/prob1.agda	Tue Nov 26 16:23:35 2019 +0900
@@ -66,6 +66,10 @@
 <-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
 <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {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
+x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
+
 -- <-plus-0 (subst₂ ( λ j k → j < k ) (+-comm _  _ ) (+-comm _ _) (<-plus-0 {x} {y} {z} lt ) )
 
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
@@ -74,11 +78,11 @@
 minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
 minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
            minus (minus x y) z + z
-        ≡⟨ minus+n {_} {z} {!!} ⟩
+        ≡⟨ minus+n {_} {z} lemma ⟩
            minus x y
         ≡⟨ +m= {_} {_} {y} ( begin
               minus x y + y 
-           ≡⟨ minus+n {_} {y} {!!} ⟩
+           ≡⟨ minus+n {_} {y} lemma1 ⟩
               x
            ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
               minus x (z + y) + (z + y)
@@ -90,10 +94,10 @@
            minus x (y + z) + z
         ∎  ) where
              open ≡-Reasoning
+             lemma1 : suc x > y
+             lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt )
              lemma : suc (minus x y) > z
-             lemma = <-minus {_} {_} {y} ?
-             lemma1 : suc x > y
-             lemma1 = {!!}
+             lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y}  lemma1 ))  gt )
 
 minus-* : {M k n : ℕ } → minus k (suc n) * M ≡ minus (minus k n * M ) M
 minus-* {M} {k} {n} = begin