--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/BinaryTree.agda	Fri Aug 14 18:07:49 2020 +0900
@@ -0,0 +1,71 @@
+open import Level renaming (suc to Suc ; zero to Zero )
+module BinaryTree  where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat hiding (compare)
+open import Data.Maybe
+open import Data.List
+open import Function
+open import logic
+open import nat
+open import Data.Nat.Properties
+
+open import Stack
+open Stack.Stack
+
+data Node {n : Level }  (a : Set n)  : Set n where
+  empty : Node a
+  node  : ℕ → a → Node  a → Node a → Node a
+
+record BinaryTree {n m : Level } (a : Set n ) {t : Set m }  : Set (m Level.⊔ (Suc n)) where
+  field
+    tree : Node a
+  findNode : ℕ → Node a  → Stack (Node a) {t} → ( Stack (Node a) {t} → t ) → t 
+  findNode k empty s next = next s
+  findNode k (node k1 d1 left right) s next  with <-cmp k k1
+  ... | tri< a ¬b ¬c = pushStack s (node k1 d1 left right) $ λ s →  findNode k left s next 
+  ... | tri≈ ¬a b ¬c = pushStack s (node k1 d1 left right)  next
+  ... | tri> ¬a ¬b c = pushStack s (node k1 d1 left right) $ λ s →  findNode k right s next 
+  replaceNode : ℕ → a → (BinaryTree a {t} → t) → Stack ( Node a) {t} → t
+  replaceNode k d next s = replaceNode1 (stack s) (node k d empty empty) next where
+     -- if we use stack API, termination check may fail
+     replaceNode1 : List (Node a) → Node a → (BinaryTree a {t} → t) → t
+     replaceNode1 [] r next = next record { tree = r }
+     replaceNode1 (empty ∷ t) r next = replaceNode1 t r next
+     replaceNode1 (node k1 d1 left right ∷ t) r next with <-cmp k k1
+     ... | tri< a ¬b ¬c = replaceNode1 t (node k1 d1 r right) next
+     ... | tri≈ ¬a b ¬c = replaceNode1 t (node k d left right) next
+     ... | tri> ¬a ¬b c = replaceNode1 t (node k1 d1 left r ) next
+  putTree : ℕ → a → (BinaryTree a {t} → t) → t
+  putTree k d next = findNode k tree  (createSingleLinkedStack (Node a)) $ replaceNode k d next 
+  getTree : ℕ → (BinaryTree a {t} → Maybe a → t) → t
+  getTree k next = getTree1 k tree next where
+     getTree1 : ℕ → Node a  → (BinaryTree a {t} → Maybe a → t) → t
+     getTree1 k empty next = next record { tree = tree } nothing
+     getTree1 k (node k1 d1 left right) next  with <-cmp k k1
+     ... | tri< a ¬b ¬c = getTree1 k left next 
+     ... | tri≈ ¬a b ¬c = next record { tree = tree } ( just d1 )
+     ... | tri> ¬a ¬b c = getTree1 k right next 
+     
+  -- rmTree : ℕ → (BinaryTree a {t} → t) → t
+  -- rmTree k next = {!!}
+  -- clearTree : (BinaryTree  a {t}   → t) → t
+  -- clearTree next = next {!!}
+
+open BinaryTree
+
+createBinaryTree : {n m : Level } {t : Set m } (a : Set n) → BinaryTree {n} {m} a {t} 
+createBinaryTree a = record { tree = empty }
+
+test3 : Maybe ℕ
+test3 = putTree (createBinaryTree ℕ) 1 1 $ λ s → putTree s 2 2 $ λ s → getTree s 2 ( λ s a → a  )
+
+test4 : Node ℕ
+test4 = putTree (createBinaryTree ℕ) 1 1
+    $ λ s → putTree s 2 2
+    $ λ s → putTree s 5 3
+    $ λ s → putTree s 4 4
+    $ λ s → putTree s 4 5
+    $ λ s → getTree s 5 ( λ s a → tree s  )
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Fib.agda	Fri Aug 14 18:07:49 2020 +0900
@@ -0,0 +1,48 @@
+open import Level renaming (suc to Suc ; zero to Zero )
+module Fib where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat hiding (compare)
+open import Data.Maybe
+open import Data.List
+open import Function
+open import logic
+
+record Fib {m : Level }  {t : Set m }  : Set m where
+
+  fib0 : ℕ → (ℕ → t) → t
+  fib0 i next = next (fib01 i) where
+      fib01 : ℕ → ℕ
+      fib01 zero = zero
+      fib01 (suc zero) = 1
+      fib01 (suc (suc i)) = fib01 i + fib01 (suc i)
+
+  fib1 : ℕ → (ℕ → t) → t
+  fib1 i next = fib11 i 1 zero next where
+      fib11 : ( i a b : ℕ ) → (ℕ → t) → t
+      fib11 zero a b next = next b
+      fib11 (suc i) a b next = fib11 i b ( a + b ) next
+
+  fib2 : ℕ → (ℕ → t) → t
+  fib2 i next = fib21 i next where
+      fib21 : ( i : ℕ ) → (ℕ → t) → t
+      fib21 zero next = next 0
+      fib21 (suc zero) next = next 1
+      -- this is not a tail call (why?)
+      fib21 (suc (suc i)) next = fib21 i $ λ j → fib21 (suc i) $ λ k → next ( j + k )
+
+open Fib
+
+createFib : {m : Level } {t : Set m }  → Fib {m} {t} 
+createFib = record { }
+
+test2 : ℕ
+test2 = fib0 createFib 10 $ λ i → i
+
+test3 : ℕ
+test3 = fib1 createFib 10 $ λ i → i
+
+test4 : ℕ
+test4 = fib2 createFib 10 $ λ i → i
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Stack.agda	Fri Aug 14 18:07:49 2020 +0900
@@ -0,0 +1,46 @@
+open import Level renaming (suc to Suc ; zero to Zero )
+module Stack  where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat hiding (compare)
+open import Data.Maybe
+open import Data.List
+open import Function
+open import logic
+
+record Stack {n m : Level } (a : Set n ) {t : Set m }  : Set (m Level.⊔ (Suc n)) where
+  field
+    stack : List a
+
+  pushStack :  a → (Stack a {t} → t) → t
+  pushStack d next = next ( record { stack = d ∷ stack } )
+
+  popStack : (Stack a {t} → Maybe a  → t) → t
+  popStack next with stack
+  popStack next | [] = next record { stack = [] } nothing
+  popStack next | x ∷ t = next record { stack = t } (just x)
+
+  pop2Stack :  (Stack a {t}  → Maybe a → Maybe a → t) → t
+  pop2Stack next with stack
+  pop2Stack next | x ∷ x₁ ∷ t = next record { stack = t } (just x) (just x₁)
+  pop2Stack next | x ∷ [] = next record { stack = [] } (just x) nothing
+  pop2Stack next | _ =  next record {stack = stack} nothing nothing
+
+  get2Stack :  (Stack a {t}  → Maybe a → Maybe a → t) → t
+  get2Stack next with stack
+  get2Stack next | x ∷ x₁ ∷ t = next record { stack = stack } (just x) (just x₁)
+  get2Stack next | x ∷ [] = next record { stack = stack } (just x) nothing
+  get2Stack next | _ =  next record {stack = stack } nothing nothing
+
+  clearStack : (Stack a {t}   → t) → t
+  clearStack next = next record { stack = [] } 
+
+open Stack
+
+createSingleLinkedStack : {n m : Level } {t : Set m } (a : Set n) → Stack {n} {m} a {t} 
+createSingleLinkedStack a = record { stack = [] }
+
+test2 : List (Maybe ℕ)
+test2 = pushStack (createSingleLinkedStack ℕ) 1 $ λ s → pushStack s 2 $ λ s → pop2Stack s ( λ s a b → a ∷ b ∷ [] )
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/WhileTest.agda	Fri Aug 14 18:07:49 2020 +0900
@@ -0,0 +1,39 @@
+open import Level renaming (suc to Suc ; zero to Zero )
+module WhileTest  where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat hiding (compare)
+open import Data.Maybe
+open import Data.List
+open import Function
+open import logic
+
+record Env : Set (Suc Zero) where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
+
+record WhileTest {m : Level }  {t : Set m }  : Set (Suc m) where
+  field
+    env : Env
+  whileInit : (c10 : ℕ) → (Env → t) → t
+  whileInit c10 next = next (record {varn = c10 ; vari = 0 } )
+  whileLoop : Env → (Code : Env → t) → t
+  whileLoop env next = whileLoop1 (varn env) env where
+      whileLoop1 : ℕ → Env → t
+      whileLoop1 zero env =  next env
+      whileLoop1 (suc t ) env = 
+          whileLoop1 t (record env {varn = t ; vari = (vari env) + 1}) 
+  whileTest : (c10 : ℕ) → (Env → t) → t
+  whileTest c10 next = whileInit c10 $ λ env → whileLoop env next
+
+open WhileTest
+
+createWhileTest : {m : Level} {t : Set m }  → WhileTest {m} {t}
+createWhileTest  = record { env = record { varn = 0; vari = 0 } }
+
+test2 : ℕ
+test2 = whileTest createWhileTest 10 $ λ e → vari e
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/logic.agda	Fri Aug 14 18:07:49 2020 +0900
@@ -0,0 +1,152 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool → Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _/\_
+
+open import Relation.Binary.PropositionalEquality
+
+
+≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
+≡-Bool-func {true} {true} a→b b→a = refl
+≡-Bool-func {false} {true} a→b b→a with b→a refl
+... | ()
+≡-Bool-func {true} {false} a→b b→a with a→b refl
+... | ()
+≡-Bool-func {false} {false} a→b b→a = refl
+
+bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
+bool-≡-? true true = yes refl
+bool-≡-? true false = no (λ ())
+bool-≡-? false true = no (λ ())
+bool-≡-? false false = yes refl
+
+¬-bool-t : {a : Bool} →  ¬ ( a ≡ true ) → a ≡ false
+¬-bool-t {true} ne = ⊥-elim ( ne refl )
+¬-bool-t {false} ne = refl
+
+¬-bool-f : {a : Bool} →  ¬ ( a ≡ false ) → a ≡ true
+¬-bool-f {true} ne = refl
+¬-bool-f {false} ne = ⊥-elim ( ne refl )
+
+¬-bool : {a : Bool} →  a ≡ false  → a ≡ true → ⊥
+¬-bool refl ()
+
+lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
+lemma-∧-0 {true} {true} refl ()
+lemma-∧-0 {true} {false} ()
+lemma-∧-0 {false} {true} ()
+lemma-∧-0 {false} {false} ()
+
+lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
+lemma-∧-1 {true} {true} refl ()
+lemma-∧-1 {true} {false} ()
+lemma-∧-1 {false} {true} ()
+lemma-∧-1 {false} {false} ()
+
+bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
+bool-and-tt refl refl = refl
+
+bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 
+bool-∧→tt-0 {true} {true} refl = refl
+bool-∧→tt-0 {false} {_} ()
+
+bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 
+bool-∧→tt-1 {true} {true} refl = refl
+bool-∧→tt-1 {true} {false} ()
+bool-∧→tt-1 {false} {false} ()
+
+bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
+bool-or-1 {false} {true} refl = refl
+bool-or-1 {false} {false} refl = refl
+bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 
+bool-or-2 {true} {false} refl = refl
+bool-or-2 {false} {false} refl = refl
+
+bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 
+bool-or-3 {true} = refl
+bool-or-3 {false} = refl
+
+bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true 
+bool-or-31 {true} {true} refl = refl
+bool-or-31 {false} {true} refl = refl
+
+bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
+bool-or-4 {true} = refl
+bool-or-4 {false} = refl
+
+bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true 
+bool-or-41 {true} {b} refl = refl
+
+bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
+bool-and-1 {false} {b} refl = refl
+bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
+bool-and-2 {true} {false} refl = refl
+bool-and-2 {false} {false} refl = refl
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nat.agda	Fri Aug 14 18:07:49 2020 +0900
@@ -0,0 +1,355 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module nat where
+
+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
+-- open import Relation.Binary.Definitions
+
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = 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 : ℕ } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
+¬a≤a  (s≤s lt) = ¬a≤a  lt
+
+a<sa : {la : ℕ} → la < suc la 
+a<sa {zero} = s≤s z≤n
+a<sa {suc la} = s≤s a<sa 
+
+=→¬< : {x : ℕ  } → ¬ ( x < x )
+=→¬< {zero} ()
+=→¬< {suc x} (s≤s lt) = =→¬< lt
+
+>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
+>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
+
+<-∨ : { 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 : ℕ) → ℕ
+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 )
+
+-- _*_ : ℕ → ℕ → ℕ
+-- _*_ zero _ = zero
+-- _*_ (suc n) m = m + ( 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
+
+
+-- open import Relation.Binary.PropositionalEquality
+
+-- postulate extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
+
+-- <-≡-iff : {A B : (a b : ℕ ) → Set } → {a b : ℕ }  → (A a b → B a b ) → (B a b → A a b ) → A ≡ B
+-- <-≡-iff {A} {B} ab ba = {!!}
+
+
+0<s : {x : ℕ } → zero < suc x
+0<s {_} = s≤s z≤n 
+
+<-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 : {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)
+
+<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y 
+<-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )
+
+<<+ : {x y z w : ℕ } → x < y → w < z  → x + w < y + z 
+<<+ {x} {y} {z} {w} x<y w<z = <-trans ( <-plus {_} {_} {w } x<y ) ( <-plus-0 w<z )
+
+≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
+≤-plus {0} {y} {zero} z≤n = z≤n
+≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y 
+≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )
+
+≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y 
+≤-plus-0 {x} {y} {zero} lt = lt
+≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )
+
+<≤+ : {x y z w : ℕ } → x < y → w ≤ z  → x + w < y + z 
+<≤+ {x} {y} {z} {w} x<y w≤z  = ≤-trans ( <-plus {_} {_} {w } x<y ) ( ≤-plus-0 w≤z )
+
+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 )
+
+≤-minus-0 : {x y z : ℕ } → z + x ≤ z + y → x ≤ y
+≤-minus-0 {x} {y} {zero} lt = lt
+≤-minus-0 {x} {y} {suc z} (s≤s lt) = ≤-minus-0 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+y≤z→x≤z : {x y z : ℕ } → x + y ≤ z → x ≤ z 
+x+y≤z→x≤z {zero} z≤n = z≤n
+x+y≤z→x≤z {zero} (s≤s lt) = z≤n
+x+y≤z→x≤z {suc x} (s≤s lt) = s≤s ( x+y≤z→x≤z lt )
+
+*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
+*≤ lt = *-mono-≤ lt ≤-refl
+
+≤* : {x y z : ℕ } → x ≤ y → z * x ≤ z * y 
+≤* {x} {y} {z} lt = subst₂ (λ x y → x ≤ y ) (*-comm _ z)  (*-comm _ z) (*≤ lt)
+
+*< : {x y z : ℕ } → x < y → x * suc z < y * suc z 
+*< {zero} {suc y} lt = s≤s z≤n
+*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
+
+<* : {x y z : ℕ } → x < y → suc z * x <  suc z * y
+<* {x} {y} {z} lt =  subst₂ (λ x y → x < y ) (*-comm x _ ) (*-comm y (suc z)) (*< lt)
+
+<to<s : {x y  : ℕ } → x < y → x < suc y
+<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
+<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
+
+<tos<s : {x y  : ℕ } → x < y → suc x < suc y
+<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
+<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)
+
+≤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
+
+minus>0 : {x y : ℕ } → x < y → 0 < minus y x 
+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
+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 = 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
+           minus k (suc n) * zero
+        ≡⟨ *-comm (minus k (suc n)) zero ⟩
+           zero * minus k (suc n) 
+        ≡⟨⟩
+           0 * minus k n 
+        ≡⟨ *-comm 0 (minus k n) ⟩
+           minus (minus k n * 0 ) 0
+        ∎  where
+        open ≡-Reasoning
+minus-* {suc m} {k} {n} lt with <-cmp k 1
+minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
+minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
+minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
+minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt 
+minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
+minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = 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} (lemma 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
+             M = suc m
+             lemma : {n k m : ℕ } → n < k  → suc (k * suc m) > suc m + n * suc m
+             lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
+             lemma {suc n} {suc k} {m} lt = begin
+                         suc (suc m + suc n * suc m) 
+                      ≡⟨⟩
+                         suc ( suc (suc n) * suc m)
+                      ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
+                         suc (suc k * suc m)
+                      ∎   where open ≤-Reasoning
+             open ≡-Reasoning