Mercurial > hg > Members > kono > Proof > prob1

changeset 14:8415d3f77fe0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minus clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 27 Nov 2019 09:59:51 +0900
parents 0e63ca7fd224
children 559bada080d5
files nat.agda prob1.agda
diffstat 2 files changed, 237 insertions(+), 230 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Wed Nov 27 09:35:08 2019 +0900
+++ b/nat.agda	Wed Nov 27 09:59:51 2019 +0900
@@ -1,56 +1,225 @@
 module nat where
 
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Nat 
+open import Data.Nat.Properties
 open import Data.Empty
 open import Relation.Nullary
 open import  Relation.Binary.PropositionalEquality
+open import  Relation.Binary.Core
 open import  logic
 
 
-nat-<> : { x y : Nat } → x < y → y < x → ⊥
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 
-nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥
+nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
 nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
 
-nat-<≡ : { x : Nat } → x < x → ⊥
+nat-<≡ : { x : ℕ } → x < x → ⊥
 nat-<≡  (s≤s lt) = nat-<≡ lt
 
-nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
 nat-≡< refl lt = nat-<≡ lt
 
-¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
+¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
 ¬a≤a  (s≤s lt) = ¬a≤a  lt
 
-a<sa : {la : Nat} → la < Suc la 
-a<sa {Zero} = s≤s z≤n
-a<sa {Suc la} = s≤s a<sa 
+a<sa : {la : ℕ} → la < suc la 
+a<sa {zero} = s≤s z≤n
+a<sa {suc la} = s≤s a<sa 
 
-=→¬< : {x : Nat  } → ¬ ( x < x )
-=→¬< {Zero} ()
-=→¬< {Suc x} (s≤s lt) = =→¬< lt
+=→¬< : {x : ℕ  } → ¬ ( x < x )
+=→¬< {zero} ()
+=→¬< {suc x} (s≤s lt) = =→¬< lt
 
->→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
+>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
 
-<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
-<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
-<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
-<-∨ {Suc x} {Zero} (s≤s ())
-<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
-<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
-<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ {zero} {zero} (s≤s z≤n) = case1 refl
+<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
+<-∨ {suc x} {zero} (s≤s ())
+<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
+<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
+<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
 
-max : (x y : Nat) → Nat
-max Zero Zero = Zero
-max Zero (Suc x) = (Suc x)
-max (Suc x) Zero = (Suc x)
-max (Suc x) (Suc y) = Suc ( max x y )
+max : (x y : ℕ) → ℕ
+max zero zero = zero
+max zero (suc x) = (suc x)
+max (suc x) zero = (suc x)
+max (suc x) (suc y) = suc ( max x y )
 
--- _*_ : Nat → Nat → Nat
+-- _*_ : ℕ → ℕ → ℕ
 -- _*_ zero _ = zero
 -- _*_ (suc n) m = m + ( n * m )
 
-exp : Nat → Nat → Nat
-exp _ Zero = 1
-exp n (Suc m) = n * ( exp n m )
+exp : ℕ → ℕ → ℕ
+exp _ zero = 1
+exp n (suc m) = n * ( exp n m )
+
+minus : (a b : ℕ ) →  ℕ
+minus a zero = a
+minus zero (suc b) = zero
+minus (suc a) (suc b) = minus a b
+
+_-_ = minus
+
+m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
+m+= {i} {j} {zero} refl = refl
+m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
+
++m= : {i j  m : ℕ } → i + m ≡ j + m → i ≡ j
++m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
+
+less-1 :  { n m : ℕ } → suc n < m → n < m
+less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
+less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
+
+sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
+sa=b→a<b {0} {suc zero} refl = s≤s z≤n
+sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)
+
+minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
+minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
+minus+n {zero} {suc y} (s≤s ())
+minus+n {suc x} {suc y} (s≤s lt) = begin
+           minus (suc x) (suc y) + suc y
+        ≡⟨ +-comm _ (suc y)    ⟩
+           suc y + minus x y 
+        ≡⟨ cong ( λ k → suc k ) (
+           begin
+                 y + minus x y 
+              ≡⟨ +-comm y  _ ⟩
+                 minus x y + y
+              ≡⟨ minus+n {x} {y} lt ⟩
+                 x 
+           ∎  
+           ) ⟩
+           suc x
+        ∎  where open ≡-Reasoning
+
+<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
+<-minus-0 {x} {suc _} {zero} lt = lt
+<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
+
+<-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 {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 )
+
+*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
+*≤ lt = *-mono-≤ lt ≤-refl
+
+≤to< : {x y  : ℕ } → x < y → x ≤ y 
+≤to< {zero} {suc y} (s≤s z≤n) = z≤n
+≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y}  lt)
+
+refl-≤s : {x : ℕ } → x ≤ suc x
+refl-≤s {zero} = z≤n
+refl-≤s {suc x} = s≤s (refl-≤s {x})
+
+x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
+x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
+x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
+
+open import Data.Product
+
+minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
+minus<=0 {0} {zero} z≤n = refl
+minus<=0 {0} {suc y} z≤n = refl
+minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
+
+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
+distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
+          minus x (suc y) * z
+        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
+           0 * z 
+        ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
+          minus (x * z) (z + y * z) 
+        ∎  where
+            open ≡-Reasoning
+            le : x * z ≤ z + y * z
+            le  = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
+               lemma : x * z ≤ y * z
+               lemma = *≤ {x} {y} {z} (≤to< a)
+distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
+          minus x (suc y) * z
+        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
+           0 * z 
+        ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
+          minus (x * z) (z + y * z) 
+        ∎  where
+            open ≡-Reasoning
+            lt : {x z : ℕ } →  x * z ≤ z + x * z
+            lt {zero} {zero} = z≤n
+            lt {suc x} {zero} = lt {x} {zero}
+            lt {x} {suc z} = ≤-trans lemma refl-≤s where
+               lemma : x * suc z ≤   z + x * suc z
+               lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) 
+distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
+           minus x (suc y) * z + suc y * z
+        ≡⟨ sym (proj₂ *-distrib-+ z  (minus x (suc y) )  _) ⟩
+           ( minus x (suc y) + suc y ) * z
+        ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c))  ⟩
+           x * z 
+        ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
+           minus (x * z) (suc y * z) + suc y * z
+        ∎ ) where
+            open ≡-Reasoning
+            lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
+            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-* : {M k n : ℕ } → suc (k * M) > M + n * M → minus k (suc n) * M ≡ minus (minus k n * M ) M
+minus-* {M} {k} {n} lt = begin
+           minus k (suc n) * M
+        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
+           minus (k * M ) ((suc n) * M)
+        ≡⟨⟩
+           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} lt ) ⟩
+           minus (minus (k * M ) (n * M)) M
+        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
+           minus (minus k n * M ) M
+        ∎  where open ≡-Reasoning
+
--- a/prob1.agda	Wed Nov 27 09:35:08 2019 +0900
+++ b/prob1.agda	Wed Nov 27 09:59:51 2019 +0900
@@ -7,171 +7,9 @@
 open import logic
 open import nat
 open import Data.Empty
+open import Data.Product
 open import Relation.Nullary
 
-minus : (a b : ℕ ) →  ℕ
-minus a zero = a
-minus zero (suc b) = zero
-minus (suc a) (suc b) = minus a b
-
-m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
-m+= {i} {j} {zero} refl = refl
-m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
-
-+m= : {i j  m : ℕ } → i + m ≡ j + m → i ≡ j
-+m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
-
-less-1 :  { n m : ℕ } → suc n < m → n < m
-less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
-less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
-
-sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
-sa=b→a<b {0} {suc zero} refl = s≤s z≤n
-sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)
-
-minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
-minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
-minus+n {zero} {suc y} (s≤s ())
-minus+n {suc x} {suc y} (s≤s lt) = begin
-           minus (suc x) (suc y) + suc y
-        ≡⟨ +-comm _ (suc y)    ⟩
-           suc y + minus x y 
-        ≡⟨ cong ( λ k → suc k ) (
-           begin
-                 y + minus x y 
-              ≡⟨ +-comm y  _ ⟩
-                 minus x y + y
-              ≡⟨ minus+n {x} {y} lt ⟩
-                 x 
-           ∎  
-           ) ⟩
-           suc x
-        ∎  where open ≡-Reasoning
-
-<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
-<-minus-0 {x} {suc _} {zero} lt = lt
-<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
-
-<-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 {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 )
-
-*< : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
-*< lt = *-mono-≤ lt ≤-refl
-
-≤to< : {x y  : ℕ } → x < y → x ≤ y 
-≤to< {zero} {suc y} (s≤s z≤n) = z≤n
-≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y}  lt)
-
-refl-≤s : {x : ℕ } → x ≤ suc x
-refl-≤s {zero} = z≤n
-refl-≤s {suc x} = s≤s (refl-≤s {x})
-
-x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
-x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
-x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
-
-open import Data.Product
-
-minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
-minus<=0 {0} {zero} z≤n = refl
-minus<=0 {0} {suc y} z≤n = refl
-minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
-
-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
-distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
-          minus x (suc y) * z
-        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
-           0 * z 
-        ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
-          minus (x * z) (z + y * z) 
-        ∎  where
-            open ≡-Reasoning
-            le : x * z ≤ z + y * z
-            le  = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
-               lemma : x * z ≤ y * z
-               lemma = *< {x} {y} {z} (≤to< a)
-distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
-          minus x (suc y) * z
-        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
-           0 * z 
-        ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
-          minus (x * z) (z + y * z) 
-        ∎  where
-            open ≡-Reasoning
-            lt : {x z : ℕ } →  x * z ≤ z + x * z
-            lt {zero} {zero} = z≤n
-            lt {suc x} {zero} = lt {x} {zero}
-            lt {x} {suc z} = ≤-trans lemma refl-≤s where
-               lemma : x * suc z ≤   z + x * suc z
-               lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) 
-distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
-           minus x (suc y) * z + suc y * z
-        ≡⟨ sym (proj₂ *-distrib-+ z  (minus x (suc y) )  _) ⟩
-           ( minus x (suc y) + suc y ) * z
-        ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c))  ⟩
-           x * z 
-        ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
-           minus (x * z) (suc y * z) + suc y * z
-        ∎ ) where
-            open ≡-Reasoning
-            lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
-            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-* : {M k n : ℕ } → suc (k * M) > M + n * M → minus k (suc n) * M ≡ minus (minus k n * M ) M
-minus-* {M} {k} {n} lt = begin
-           minus k (suc n) * M
-        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
-           minus (k * M ) ((suc n) * M)
-        ≡⟨⟩
-           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} lt ) ⟩
-           minus (minus (k * M ) (n * M)) M
-        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
-           minus (minus k n * M ) M
-        ∎  where open ≡-Reasoning
 
 -- All variables are positive integer
 -- A = -M*n + i +k*M  - M
@@ -205,70 +43,70 @@
 problem0-k=k (suc k) A zero A<kM = {!!} 
 problem0-k=k (suc k) A (suc m) A<kM = cc k a<sa (start-range k) where
      M = suc m
-     cck :  ( n : ℕ ) →  n < suc k  → (suc A >  (minus k n ) * M )  → minus A (minus k n * M) < M →  Cond1 A M (suc k)
-     cck n n<k gt lt =  record { n = n ; i = minus A ((minus k n) * M ) ; range-n = n<k   ; range-i = lt ; rule1 = lemma2 }  where
-        lemma2 :   minus A (minus k n * M) + suc k * M ≡ M * suc n + A
+     cck :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M →  Cond1 A M (suc k)
+     cck n n<k gt lt =  record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = lt ; rule1 = lemma2 }  where
+        lemma2 :   A - ((k - n) * M) + suc k * M ≡ M * suc n + A
         lemma2 = begin
-           minus A (minus k n * M) + suc k * M                 ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩
-           minus A (minus k n * M) + (suc ((minus k n ) + n )) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (+-comm _ n) ⟩
-           minus A (minus k n * M) + (suc (n + (minus k n ) )) * M ≡⟨⟩
-           minus A (minus k n * M) + (suc n + (minus k n ) ) * M   ≡⟨ cong ( λ x → minus A (minus k n * M) + x * M ) (+-comm (suc n) _) ⟩
-           minus A (minus k n * M) + ((minus k n ) + suc n ) * M   ≡⟨ cong ( λ x → minus A (minus k n * M) + x  ) (((proj₂ *-distrib-+)) M (minus k n)  _  ) ⟩
-           minus A (minus k n * M) + ((minus k n * M) + (suc n) * M) ≡⟨ sym (+-assoc (minus A (minus k n * M)) _ ((suc n) * M)) ⟩
-           minus A (minus k n * M) + (minus k n * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {minus k n * M}  gt ) ⟩
+           A - ((k - n) * M) + suc k * M                           ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩
+           A - ((k - n) * M) + (suc (((k - n) ) + n )) * M         ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (+-comm _ n) ⟩
+           A - ((k - n) * M) + (suc (n + ((k - n) ) )) * M         ≡⟨⟩
+           A - ((k - n) * M) + (suc n + ((k - n) ) ) * M           ≡⟨ cong ( λ x → A - ((k - n) * M) + x * M ) (+-comm (suc n) _) ⟩
+           A - ((k - n) * M) + (((k - n) ) + suc n ) * M           ≡⟨ cong ( λ x → A - ((k - n) * M) + x  ) (((proj₂ *-distrib-+)) M ((k - n))  _  ) ⟩
+           A - ((k - n) * M) + (((k - n) * M) + (suc n) * M)       ≡⟨ sym (+-assoc (A - ((k - n) * M)) _ ((suc n) * M)) ⟩
+           A - ((k - n) * M) + ((k - n) * M) + (suc n) * M         ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {(k - n) * M}  gt ) ⟩
            A + (suc n) * M                                         ≡⟨ cong ( λ k → A + k ) (*-comm (suc n)  _ )  ⟩
            A + M * (suc n)                                         ≡⟨ +-comm A _ ⟩
            M * (suc n) + A
           ∎  where open ≡-Reasoning
-     --  loop on  range  of A : (minus k n ) * M ≤ A < (minus k n ) * M + M
-     nextc : (n : ℕ ) → (suc n < suc k) → suc (minus k n * M) > M --  M + n * M < suc (minus k n * M) + n * M
+     --  loop on  range  of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M
+     nextc : (n : ℕ ) → (suc n < suc k) → suc ((k - n) * M) > M --  M + n * M < suc ((k - n) * M) + n * M
      nextc n n<k = <-minus {_} {_} {n * M} ( subst ( λ x → M + n * M < suc x + n * M ) (sym ( distr-minus-* {k} {n} {M} )) lemma ) where
-          lemma : M + n * M < suc (minus (k * M) (n * M)) + n * M
+          lemma : M + n * M < suc ((k * M) - (n * M)) + n * M
           lemma = subst ( λ x → suc n * M < suc x ) (sym (minus+n {k * M} {n * M} {!!})) {!!}
-     cc : (n : ℕ) → n < suc k → suc A > minus k n * M → Cond1 A M (suc k)
+     cc : (n : ℕ) → n < suc k → suc A > (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 
         a<m = A<kM
-        lemma : minus A (minus k 0 * M) < M
+        lemma : A - ((k - 0) * M) < M
         lemma = <-minus {_} {_} {k * M} (subst (λ x → x < M + k * M) (sym (minus+n {A} {k * M} k<A )) (less-1 a<m) )
-     cc (suc n) n<k k<A with <-cmp (minus A (minus k (suc n) * M))  M
+     cc (suc n) n<k k<A with <-cmp (A - ((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
-        a=mk0 :  (minus A (minus k (suc n) * M)) ≡  M → A ≡ minus k n * M
+        a=mk0 :  (A - ((k - (suc n)) * M)) ≡  M → A ≡ (k - n) * M
         a=mk0 a=mk = sym ( begin
-           minus k n * M 
-         ≡⟨ sym ( minus+n {minus k n * M} {M} (nextc n n<k )) ⟩
-           minus (minus k n * M ) M + M
+           (k - n) * M 
+         ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩
+           ((k - n) * M ) - M + M
          ≡⟨ +-comm _ M ⟩
-           M + minus (minus k n * M ) M
+           M + (((k - n) * M ) - M)
          ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} {!!}  )) ⟩
-           M + (minus k (suc n) * M) 
-         ≡⟨ cong (λ x → x + minus k (suc n) * M) (sym a=mk) ⟩
-           minus A (minus k (suc n) * M) + (minus k (suc n) * M) 
-         ≡⟨ minus+n {A} {minus k (suc n) * M} k<A ⟩
+           M + (k - (suc n) * M) 
+         ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩
+           A - ((k - (suc n)) * M) + ((k - (suc n)) * M) 
+         ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩
            A
          ∎ ) where open ≡-Reasoning
-        lemma1 : (minus A (minus k (suc n) * M)) ≡  M → suc A > minus k n * M
-        lemma1 a=mk = subst (λ x → minus k n * M < suc x ) (sym (a=mk0 a=mk )) a<sa
+        lemma1 : (A - ((k - (suc n)) * M)) ≡  M → suc A > (k - n) * M
+        lemma1 a=mk = subst (λ x → (k - n) * M < suc x ) (sym (a=mk0 a=mk )) a<sa
      cc (suc n) n<k k<A | tri> ¬a ¬b c = cc n (less-1 n<k) (lemma3 c) where
-        -- 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
+        -- A > M + (k - (suc n)) * M → A > M + (k - n) - M → A >  (k - n)
+        lemma3 : (A - ((k - (suc n)) * M)) > M  → suc A > (k - n) * M
         lemma3 mk<a = <-trans lemma5 a<sa where
-            lemma6 :  M + minus k (suc n) * M ≡ minus k n * M
+            lemma6 :  M + (k - (suc n)) * M ≡ (k - n) * M
             lemma6 = begin
-                  M + minus k (suc n) * M 
+                  M + (k - (suc n)) * M 
                ≡⟨ cong (λ x → M + x) (minus-* {M} {k} {!!} )  ⟩
-                  M + minus (minus k n * M ) M
+                  M + (((k - n) * M ) - M )
                ≡⟨ +-comm M _ ⟩
-                  minus (minus k n * M ) M + M
+                  ((k - n) * M ) - M + M
                ≡⟨ minus+n {_} {M} (nextc n n<k) ⟩
-                  minus k n * M
+                  (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} k<A ) ( <-plus mk<a )
-            lemma5 : minus k n * M < A
+            lemma4 : (M + (k - (suc n)) * M) < A
+            lemma4 = subst (λ x → (M + (k - (suc n)) * M)  < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a )
+            lemma5 : (k - n) * M < A
             lemma5 = subst (λ x → x < A ) lemma6 lemma4
-     start-range : (k : ℕ ) → suc A > minus k k * M
+     start-range : (k : ℕ ) → suc A > (k - k) * M
      start-range zero = s≤s z≤n
      start-range (suc k) = start-range k