# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585585136 -32400
# Node ID 1e313089683469b2788512c9a14ba4d630a63d51
# Parent  908409975a5ef87d749c18e02a45009636416568
maxA done (all 0,1,2 done)

diff -r 908409975a5e -r 1e3130896834 nat.agda
--- a/nat.agda	Mon Mar 30 20:22:04 2020 +0900
+++ b/nat.agda	Tue Mar 31 01:18:56 2020 +0900
@@ -204,6 +204,69 @@
 minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
 minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
 
+minus-assoc : {x y z : ℕ} → (x - y) - z ≡ x - (y + z)
+minus-assoc {x} {zero} = refl
+minus-assoc {zero} {suc y} {z} = begin
+          (zero - suc y) - z
+       ≡⟨ cong (λ k → k - z ) (minus<=0 {zero} {suc y} z≤n ) ⟩
+          zero - z
+       ≡⟨ minus<=0 {zero} {z} z≤n  ⟩
+          zero
+       ≡⟨ sym ( minus<=0 {zero} {suc y + z} z≤n ) ⟩
+          zero - (suc y + z)
+       ∎  where open ≡-Reasoning
+minus-assoc {suc x} {suc y} = minus-assoc {x} {y}
+
+minus+assoc : {x y z : ℕ } → z < suc y  → x + (y - z)  ≡ (x + y) - z
+minus+assoc {x} {y} {zero} z<y = refl
+minus+assoc {x} {suc y} {suc z} (s≤s z<y) = begin
+          x + (suc y - suc z)
+       ≡⟨⟩
+          x + (y - z)
+       ≡⟨ minus+assoc z<y ⟩
+          (x + y) - z
+       ≡⟨⟩
+          suc (x + y) - suc z
+       ≡⟨ cong (λ k → suc k - suc z) ( +-comm _ y ) ⟩
+          suc (y + x) - suc z
+       ≡⟨⟩
+          (suc y + x) - suc z
+       ≡⟨ cong (λ k → k - suc z) ( +-comm _ x ) ⟩
+          (x + suc y) - suc z
+       ∎  where open ≡-Reasoning
+
+n+0≡n : {n : ℕ } → n + 0 ≡ n
+n+0≡n {n} = trans (+-comm n 0) refl
+
+s-minus : {x y : ℕ } → x - y ≤ suc x - y
+s-minus {zero} {y} = subst (λ k → k ≤ suc zero - y  ) (sym (minus<=0 {zero} {y} z≤n) ) z≤n
+s-minus {suc x} {zero} = s≤s refl-≤s
+s-minus {suc x} {suc y} = s-minus {x} {y}
+
+minus-s : {x y : ℕ } → x - suc y ≤ x - y
+minus-s {zero} {y} = begin
+          zero - suc y
+       ≡⟨ minus<=0 {zero} {suc y} z≤n ⟩
+          zero
+       ≡⟨ sym (minus<=0 {zero} {y} z≤n) ⟩
+          zero - y
+       ∎  where open ≤-Reasoning
+minus-s {suc x} {y} = s-minus {x} {y}
+
+minus+< : {x y z : ℕ } →  x - ( y + z ) ≤ x - y
+minus+< {x} {y} {zero} = subst (λ k → x - k ≤ x - y ) (sym (n+0≡n {y})) ≤-refl
+minus+< {x} {y} {suc z} = begin
+          x - (y + suc z)
+       ≡⟨ sym (minus-assoc {x} {y} {suc z} ) ⟩
+         (x - y) - (suc z)
+       ≤⟨ minus-s {x - y} ⟩
+         (x - y) - z
+       ≡⟨ minus-assoc {x} {y} {z}  ⟩
+          x - (y + z) 
+       ≤⟨  minus+< {x} {y} {z}  ⟩
+          x - y 
+       ∎  where open ≤-Reasoning
+
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
 distr-minus-* {x} {zero} {z} = refl
 distr-minus-* {x} {suc y} {z} with <-cmp x y
@@ -247,28 +310,7 @@
             lt {x} {y} {z} le = *≤ le 
 
 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} lemma ⟩
-           minus x y
-        ≡⟨ +m= {_} {_} {y} ( begin
-              minus x y + y 
-           ≡⟨ minus+n {_} {y} lemma1 ⟩
-              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
-             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} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y}  lemma1 ))  gt )
+minus- {x} {y} {z} gt = minus-assoc {x} {y} {z}
 
 minus-* : {M k n : ℕ } → n < k  → minus k (suc n) * M ≡ minus (minus k n * M ) M
 minus-* {zero} {k} {n} lt = begin
diff -r 908409975a5e -r 1e3130896834 prob1.agda
--- a/prob1.agda	Mon Mar 30 20:22:04 2020 +0900
+++ b/prob1.agda	Tue Mar 31 01:18:56 2020 +0900
@@ -135,17 +135,31 @@
         unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c ))
         unique-n :  {j m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → n ≡ m1
         unique-n {j} {m1} j<M m1<k eq = unique-m (unique-i j<M m1<k eq ) (Cond1.rule1 c1) eq 
+        lemmab : {x m : ℕ } → x <  suc (m + x)
+        lemmab {x} {zero} =  a<sa
+        lemmab {zero} {suc m} =  <to<s (lemmab {zero} {m})
+        lemmab {suc x} {suc m} =  ( s≤s (subst (λ k → suc x ≤ k) (+-comm _ (suc m)) x≤x+y ))
+        lemmaa : {x y : ℕ} → suc x > y → (suc x - y) + y ≡ suc ( (x - y) + y )
+        lemmaa {x} {y} lt = begin
+                  (suc x - y) + y
+               ≡⟨ minus+n (<-trans lt a<sa ) ⟩
+                  suc x
+               ≡⟨ sym ( cong (λ k → suc k) ( minus+n {x} {y} lt ) ) ⟩
+                  suc (x - y) + y
+               ≡⟨⟩
+                  suc ( (x - y) + y )
+               ∎ where open ≡-Reasoning
         --   A < M + ((k - n) * M)
         --   A < suc k * M - n * M  < suc k * M - n * M
         lemma8 : A - ((k - n) * M) < M  → A < M + ((k - n) * M) 
-        lemma8 i<M with <-cmp (suc (suc A)) ( (k - n) * M )
-        lemma8 i<M | tri< a ¬b ¬c = {!!}
-        lemma8 i<M | tri≈ ¬a b ¬c = {!!}
+        lemma8 i<M with <-cmp (suc A) ( (k - n) * M )
+        lemma8 i<M | tri< a ¬b ¬c = <-minus-0 {A} {_} {suc zero} ( <-trans a (<to<s lemmab) ) 
+        lemma8 i<M | tri≈ ¬a b ¬c = <-minus-0 {A} {_} {suc zero} (subst (λ h → h < 1 + suc (m + minus k n * suc m)) (sym b) (<to<s lemmab)) where
         lemma8 i<M | tri> ¬a ¬b c = begin
                   suc A
-               ≡⟨ sym ( minus+n {suc A} {(k - n) * M} c )  ⟩
-                  (suc A - ((k - n) * M)) + (k - n) * M
-               ≡⟨ {!!}  ⟩
+               ≡⟨ sym ( minus+n {suc A} {(k - n) * M} (<-trans c a<sa) )  ⟩
+                  (suc A - ((k - n) * M)) + ((k - n) * M )
+               ≡⟨ lemmaa {A} {(k - n) * M} c ⟩
                   suc ( (A - ((k - n) * M)) + ((k - n) * M) )
                ≤⟨  ≤-plus i<M  ⟩ 
                    M + ((k - n) * M)
@@ -154,6 +168,11 @@
         lemma9 {zero} {zero} ()
         lemma9 {suc x} {zero} ()
         lemma9 {x} {suc y} (s≤s lt) = lt
+        lemmad : {n k m : ℕ} → n < suc k → n * suc m < suc ( k * suc m )
+        lemmad {n} {k} {m} n<k with <-cmp n k
+        lemmad {n} {k} {m} n<k | tri< a ¬b ¬c = <-trans ( *< a ) a<sa
+        lemmad {n} {k} {m} n<k | tri≈ ¬a refl ¬c = ≤-refl
+        lemmad {n} {k} {m} n<k | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n<k (s≤s c) )
         maxA : A - ((k - n) * M) < M  → A ≤ (suc k * M ) - 1
         maxA i<M = begin
                   A
@@ -161,13 +180,15 @@
                   (M + ((k - n) * M)) - 1
                ≡⟨ cong (λ k → (M + k ) - 1 ) (distr-minus-* {k} {n} {M} ) ⟩ 
                   (M + ((k * M) - ( n * M))) - 1
-               ≡⟨ {!!} ⟩ 
+               ≡⟨ cong (λ k → k - 1 ) ( minus+assoc {M} {k * M} {n * M} (lemmad n<k)) ⟩  
                   ((M + (k * M) )- ( n * M)) - 1
                ≡⟨⟩ 
                   ((suc k * M )- ( n * M)) - 1
-               ≡⟨ {!!} ⟩ 
+               ≡⟨ minus-assoc {suc k * M} {n * M} {1} ⟩ 
                   (suc k * M) - ((n * M) + 1)
-               ≤⟨ {!!}  ⟩ 
+               ≡⟨ cong (λ h → (suc k * M) - h ) (+-comm (n * M) _) ⟩ 
+                  (suc k * M) - (1 + (n * M) )
+               ≤⟨ minus+< {suc k * M} {1} {n * M} ⟩ 
                   (suc k * M ) - 1
                ∎ where open ≤-Reasoning
         c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 }