# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574747074 -32400
# Node ID c0d3c5a821dd76a22c87a1541afcc8e24fcc7986
# Parent  e0811846b2655083cc5ae394f93690df6c0a6ce0
...

diff -r e0811846b265 -r c0d3c5a821dd prob1.agda
--- a/prob1.agda	Tue Nov 26 12:42:13 2019 +0900
+++ b/prob1.agda	Tue Nov 26 14:44:34 2019 +0900
@@ -71,24 +71,29 @@
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
 distr-minus-* = {!!}
 
-minus- : {x y z : ℕ } → minus (minus x y) z ≡ minus x (y + z)
-minus- {x} {y} {z} = +m= {_} {_} {z} ( begin
+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 x y
         ≡⟨ +m= {_} {_} {y} ( begin
               minus x y + y 
-           ≡⟨ {!!}   ⟩
+           ≡⟨ minus+n {_} {y} {!!} ⟩
               x
-           ≡⟨ {!!}   ⟩
+           ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
               minus x (z + y) + (z + y)
-           ≡⟨ {!!}   ⟩
+           ≡⟨ sym ( +-assoc (minus x (z + y)) _  _ ) ⟩
               minus x (z + y) + z + y
            ∎ ) ⟩
            minus x (z + y) + z
-        ≡⟨ {!!}   ⟩
+        ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y )  ⟩
            minus x (y + z) + z
-        ∎  ) where open ≡-Reasoning
+        ∎  ) where
+             open ≡-Reasoning
+             lemma : suc (minus x y) > z
+             lemma = <-minus {_} {_} {y} ?
+             lemma1 : suc x > y
+             lemma1 = {!!}
 
 minus-* : {M k n : ℕ } → minus k (suc n) * M ≡ minus (minus k n * M ) M
 minus-* {M} {k} {n} = begin
@@ -99,7 +104,7 @@
            minus (k * M ) (M + n * M  )
         ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
            minus (k * M ) ((n * M) + M )
-        ≡⟨ sym ( minus- {k * M} {n * M} ) ⟩
+        ≡⟨ sym ( minus- {k * M} {n * M} {!!} ) ⟩
            minus (minus (k * M ) (n * M)) M
         ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
            minus (minus k n * M ) M