--- a/prob1.agda	Tue Nov 26 11:04:15 2019 +0900
+++ b/prob1.agda	Tue Nov 26 12:42:13 2019 +0900
@@ -55,14 +55,40 @@
 <-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≤x+y : {z y : ℕ } → z ≤ z + y
+x≤x+y {zero} {y} = z≤n
+x≤x+y {suc z} {y} = s≤s  (x≤x+y {z} {y})
+
+-- <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y 
+-- <-plus-0 {x} {y} {z} lt = {!!}
+
 <-plus : {x y z : ℕ } → x < y → x + z < y + z 
-<-plus = {!!}
+<-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)
+
+-- <-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) 
 distr-minus-* = {!!}
 
 minus- : {x y z : ℕ } → minus (minus x y) z ≡ minus x (y + z)
-minus- = {!!}
+minus- {x} {y} {z} = +m= {_} {_} {z} ( begin
+           minus (minus x y) z + z
+        ≡⟨ {!!}   ⟩
+           minus x y
+        ≡⟨ +m= {_} {_} {y} ( begin
+              minus x y + y 
+           ≡⟨ {!!}   ⟩
+              x
+           ≡⟨ {!!}   ⟩
+              minus x (z + y) + (z + y)
+           ≡⟨ {!!}   ⟩
+              minus x (z + y) + z + y
+           ∎ ) ⟩
+           minus x (z + y) + z
+        ≡⟨ {!!}   ⟩
+           minus x (y + z) + z
+        ∎  ) where open ≡-Reasoning
 
 minus-* : {M k n : ℕ } → minus k (suc n) * M ≡ minus (minus k n * M ) M
 minus-* {M} {k} {n} = begin
@@ -127,6 +153,8 @@
            M * (suc n) + A
           ∎  where open ≡-Reasoning
      --  loop on  range  of A : (minus k n ) * M ≤ A < (minus k n ) * M + M
+     lemma2 : (n : ℕ ) → suc (minus k n * M) > M
+     lemma2 = {!!}
      cc : (n : ℕ) → n < suc k → suc A > minus k n * M → Cond1 A M (suc k)
      cc zero n<k k<A = cck 0 n<k k<A lemma where
         a<m : suc A < M + k * M 
@@ -136,12 +164,10 @@
      cc (suc n) n<k k<A with <-cmp (minus A (minus 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 = cc n (less-1 n<k) (lemma1 b) where
-        lemma2 : suc (minus k n * M) > M
-        lemma2 = {!!}
         a=mk0 :  (minus A (minus k (suc n) * M)) ≡  M → A ≡ minus k n * M
         a=mk0 a=mk = sym ( begin
            minus k n * M 
-         ≡⟨ sym ( minus+n {minus k n * M} {M} lemma2 ) ⟩
+         ≡⟨ sym ( minus+n {minus k n * M} {M} (lemma2 n)) ⟩
            minus (minus k n * M ) M + M
          ≡⟨ +-comm _ M ⟩
            M + minus (minus k n * M ) M
@@ -158,10 +184,20 @@
         -- A > M + minus k (suc n) * M → A > M + minus k n - M → A >  minus k n
         lemma3 : (minus A (minus k (suc n) * M)) > M  → suc A > minus k n * M
         lemma3 mk<a = <-trans lemma5 a<sa where
+            lemma6 :  M + minus k (suc n) * M ≡ minus k n * M
+            lemma6 = begin
+                  M + minus k (suc n) * M 
+               ≡⟨ cong (λ x → M + x) (minus-* {M} {k}  )  ⟩
+                  M + minus (minus k n * M ) M
+               ≡⟨ +-comm M _ ⟩
+                  minus (minus k n * M ) M + M
+               ≡⟨ minus+n {_} {M} (lemma2 n) ⟩
+                  minus k n * M
+               ∎  where open ≡-Reasoning
             lemma4 : (M + minus k (suc n) * M) < A
-            lemma4 = subst (λ x → (M + minus k (suc n) * M)  < x ) (minus+n {A}{minus k (suc n) * M} {!!} ) ( <-plus mk<a )
+            lemma4 = subst (λ x → (M + minus k (suc n) * M)  < x ) (minus+n {A}{minus k (suc n) * M} k<A ) ( <-plus mk<a )
             lemma5 : minus k n * M < A
-            lemma5 = subst (λ x → x < A ) {!!} lemma4
+            lemma5 = subst (λ x → x < A ) lemma6 lemma4
      start-range : (k : ℕ ) → suc A > minus k k * M
      start-range zero = s≤s z≤n
      start-range (suc k) = start-range k