------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties about natural number operations
------------------------------------------------------------------------

-- See README.Nat for some examples showing how this module can be
-- used.

module Data.Nat.Properties where

open import Data.Nat as Nat
open ≤-Reasoning
  renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≡⟨_⟩'_)
open import Relation.Binary
open DecTotalOrder Nat.decTotalOrder using () renaming (refl to ≤-refl)
open import Function
open import Algebra
open import Algebra.Structures
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning
import Algebra.FunctionProperties as P; open P (_≡_ {A = })
open import Data.Product
open import Data.Sum

------------------------------------------------------------------------
-- (ℕ, +, *, 0, 1) is a commutative semiring

private

  +-assoc : Associative _+_
  +-assoc zero    _ _ = refl
  +-assoc (suc m) n o = cong suc $ +-assoc m n o

  +-identity : Identity 0 _+_
  +-identity =  _  refl) , n+0≡n
    where
    n+0≡n : RightIdentity 0 _+_
    n+0≡n zero    = refl
    n+0≡n (suc n) = cong suc $ n+0≡n n

  m+1+n≡1+m+n :  m n  m + suc n  suc (m + n)
  m+1+n≡1+m+n zero    n = refl
  m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)

  +-comm : Commutative _+_
  +-comm zero    n = sym $ proj₂ +-identity n
  +-comm (suc m) n =
    begin
      suc m + n
    ≡⟨ refl 
      suc (m + n)
    ≡⟨ cong suc (+-comm m n) 
      suc (n + m)
    ≡⟨ sym (m+1+n≡1+m+n n m) 
      n + suc m
    

  m*1+n≡m+mn :  m n  m * suc n  m + m * n
  m*1+n≡m+mn zero    n = refl
  m*1+n≡m+mn (suc m) n =
    begin
      suc m * suc n
    ≡⟨ refl 
      suc n + m * suc n
    ≡⟨ cong  x  suc n + x) (m*1+n≡m+mn m n) 
      suc n + (m + m * n)
    ≡⟨ refl 
      suc (n + (m + m * n))
    ≡⟨ cong suc (sym $ +-assoc n m (m * n)) 
      suc (n + m + m * n)
    ≡⟨ cong  x  suc (x + m * n)) (+-comm n m) 
      suc (m + n + m * n)
    ≡⟨ cong suc (+-assoc m n (m * n)) 
      suc (m + (n + m * n))
    ≡⟨ refl 
      suc m + suc m * n
    

  *-zero : Zero 0 _*_
  *-zero =  _  refl) , n*0≡0
    where
    n*0≡0 : RightZero 0 _*_
    n*0≡0 zero    = refl
    n*0≡0 (suc n) = n*0≡0 n

  *-comm : Commutative _*_
  *-comm zero    n = sym $ proj₂ *-zero n
  *-comm (suc m) n =
    begin
      suc m * n
    ≡⟨ refl 
      n + m * n
    ≡⟨ cong  x  n + x) (*-comm m n) 
      n + n * m
    ≡⟨ sym (m*1+n≡m+mn n m) 
      n * suc m
    

  distribʳ-*-+ : _*_ DistributesOverʳ _+_
  distribʳ-*-+ m zero    o = refl
  distribʳ-*-+ m (suc n) o =
                           begin
      (suc n + o) * m
                           ≡⟨ refl 
      m + (n + o) * m
                           ≡⟨ cong (_+_ m) $ distribʳ-*-+ m n o 
      m + (n * m + o * m)
                           ≡⟨ sym $ +-assoc m (n * m) (o * m) 
      m + n * m + o * m
                           ≡⟨ refl 
      suc n * m + o * m
                           

  *-assoc : Associative _*_
  *-assoc zero    n o = refl
  *-assoc (suc m) n o =
                         begin
    (suc m * n) * o
                         ≡⟨ refl 
    (n + m * n) * o
                         ≡⟨ distribʳ-*-+ o n (m * n) 
    n * o + (m * n) * o
                         ≡⟨ cong  x  n * o + x) $ *-assoc m n o 
    n * o + m * (n * o)
                         ≡⟨ refl 
    suc m * (n * o)
                         

isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ 0 1
isCommutativeSemiring = record
  { +-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = +-assoc
      ; ∙-cong        = cong₂ _+_
      }
    ; identityˡ = proj₁ +-identity
    ; comm      = +-comm
    }
  ; *-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = *-assoc
      ; ∙-cong        = cong₂ _*_
      }
    ; identityˡ = proj₂ +-identity
    ; comm      = *-comm
    }
  ; distribʳ = distribʳ-*-+
  ; zeroˡ    = proj₁ *-zero
  }

commutativeSemiring : CommutativeSemiring _ _
commutativeSemiring = record
  { _+_                   = _+_
  ; _*_                   = _*_
  ; 0#                    = 0
  ; 1#                    = 1
  ; isCommutativeSemiring = isCommutativeSemiring
  }

import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
module SemiringSolver =
  Solver (ACR.fromCommutativeSemiring commutativeSemiring) _≟_

------------------------------------------------------------------------
-- (ℕ, ⊔, ⊓, 0) is a commutative semiring without one

private

  ⊔-assoc : Associative _⊔_
  ⊔-assoc zero    _       _       = refl
  ⊔-assoc (suc m) zero    o       = refl
  ⊔-assoc (suc m) (suc n) zero    = refl
  ⊔-assoc (suc m) (suc n) (suc o) = cong suc $ ⊔-assoc m n o

  ⊔-identity : Identity 0 _⊔_
  ⊔-identity =  _  refl) , n⊔0≡n
    where
    n⊔0≡n : RightIdentity 0 _⊔_
    n⊔0≡n zero    = refl
    n⊔0≡n (suc n) = refl

  ⊔-comm : Commutative _⊔_
  ⊔-comm zero    n       = sym $ proj₂ ⊔-identity n
  ⊔-comm (suc m) zero    = refl
  ⊔-comm (suc m) (suc n) =
    begin
      suc m  suc n
    ≡⟨ refl 
      suc (m  n)
    ≡⟨ cong suc (⊔-comm m n) 
      suc (n  m)
    ≡⟨ refl 
      suc n  suc m
    

  ⊓-assoc : Associative _⊓_
  ⊓-assoc zero    _       _       = refl
  ⊓-assoc (suc m) zero    o       = refl
  ⊓-assoc (suc m) (suc n) zero    = refl
  ⊓-assoc (suc m) (suc n) (suc o) = cong suc $ ⊓-assoc m n o

  ⊓-zero : Zero 0 _⊓_
  ⊓-zero =  _  refl) , n⊓0≡0
    where
    n⊓0≡0 : RightZero 0 _⊓_
    n⊓0≡0 zero    = refl
    n⊓0≡0 (suc n) = refl

  ⊓-comm : Commutative _⊓_
  ⊓-comm zero    n       = sym $ proj₂ ⊓-zero n
  ⊓-comm (suc m) zero    = refl
  ⊓-comm (suc m) (suc n) =
    begin
      suc m  suc n
    ≡⟨ refl 
      suc (m  n)
    ≡⟨ cong suc (⊓-comm m n) 
      suc (n  m)
    ≡⟨ refl 
      suc n  suc m
    

  distrib-⊓-⊔ : _⊓_ DistributesOver _⊔_
  distrib-⊓-⊔ = (distribˡ-⊓-⊔ , distribʳ-⊓-⊔)
    where
    distribʳ-⊓-⊔ : _⊓_ DistributesOverʳ _⊔_
    distribʳ-⊓-⊔ (suc m) (suc n) (suc o) = cong suc $ distribʳ-⊓-⊔ m n o
    distribʳ-⊓-⊔ (suc m) (suc n) zero    = cong suc $ refl
    distribʳ-⊓-⊔ (suc m) zero    o       = refl
    distribʳ-⊓-⊔ zero    n       o       = begin
      (n  o)  0    ≡⟨ ⊓-comm (n  o) 0 
      0  (n  o)    ≡⟨ refl 
      0  n  0  o  ≡⟨ ⊓-comm 0 n  cong₂ _⊔_  ⊓-comm 0 o 
      n  0  o  0  

    distribˡ-⊓-⊔ : _⊓_ DistributesOverˡ _⊔_
    distribˡ-⊓-⊔ m n o = begin
      m  (n  o)    ≡⟨ ⊓-comm m _ 
      (n  o)  m    ≡⟨ distribʳ-⊓-⊔ m n o 
      n  m  o  m  ≡⟨ ⊓-comm n m  cong₂ _⊔_  ⊓-comm o m 
      m  n  m  o  

⊔-⊓-0-isCommutativeSemiringWithoutOne
  : IsCommutativeSemiringWithoutOne _≡_ _⊔_ _⊓_ 0
⊔-⊓-0-isCommutativeSemiringWithoutOne = record
  { isSemiringWithoutOne = record
    { +-isCommutativeMonoid = record
      { isSemigroup = record
        { isEquivalence = PropEq.isEquivalence
        ; assoc         = ⊔-assoc
        ; ∙-cong        = cong₂ _⊔_
        }
      ; identityˡ = proj₁ ⊔-identity
      ; comm      = ⊔-comm
      }
    ; *-isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = ⊓-assoc
      ; ∙-cong        = cong₂ _⊓_
      }
    ; distrib = distrib-⊓-⊔
    ; zero    = ⊓-zero
    }
  ; *-comm = ⊓-comm
  }

⊔-⊓-0-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
⊔-⊓-0-commutativeSemiringWithoutOne = record
  { _+_                             = _⊔_
  ; _*_                             = _⊓_
  ; 0#                              = 0
  ; isCommutativeSemiringWithoutOne =
      ⊔-⊓-0-isCommutativeSemiringWithoutOne
  }

------------------------------------------------------------------------
-- (ℕ, ⊓, ⊔) is a lattice

private

  absorptive-⊓-⊔ : Absorptive _⊓_ _⊔_
  absorptive-⊓-⊔ = abs-⊓-⊔ , abs-⊔-⊓
    where
    abs-⊔-⊓ : _⊔_ Absorbs _⊓_
    abs-⊔-⊓ zero    n       = refl
    abs-⊔-⊓ (suc m) zero    = refl
    abs-⊔-⊓ (suc m) (suc n) = cong suc $ abs-⊔-⊓ m n

    abs-⊓-⊔ : _⊓_ Absorbs _⊔_
    abs-⊓-⊔ zero    n       = refl
    abs-⊓-⊔ (suc m) (suc n) = cong suc $ abs-⊓-⊔ m n
    abs-⊓-⊔ (suc m) zero    = cong suc $
                   begin
      m  m
                   ≡⟨ cong (_⊓_ m) $ sym $ proj₂ ⊔-identity m 
      m  (m  0)
                   ≡⟨ abs-⊓-⊔ m zero 
      m
                   

isDistributiveLattice : IsDistributiveLattice _≡_ _⊓_ _⊔_
isDistributiveLattice = record
  { isLattice = record
      { isEquivalence = PropEq.isEquivalence
      ; ∨-comm        = ⊓-comm
      ; ∨-assoc       = ⊓-assoc
      ; ∨-cong        = cong₂ _⊓_
      ; ∧-comm        = ⊔-comm
      ; ∧-assoc       = ⊔-assoc
      ; ∧-cong        = cong₂ _⊔_
      ; absorptive    = absorptive-⊓-⊔
      }
  ; ∨-∧-distribʳ = proj₂ distrib-⊓-⊔
  }

distributiveLattice : DistributiveLattice _ _
distributiveLattice = record
  { _∨_                   = _⊓_
  ; _∧_                   = _⊔_
  ; isDistributiveLattice = isDistributiveLattice
  }

------------------------------------------------------------------------
-- Converting between ≤ and ≤′

≤-step :  {m n}  m  n  m  1 + n
≤-step z≤n       = z≤n
≤-step (s≤s m≤n) = s≤s (≤-step m≤n)

≤′⇒≤ : _≤′_  _≤_
≤′⇒≤ ≤′-refl        = ≤-refl
≤′⇒≤ (≤′-step m≤′n) = ≤-step (≤′⇒≤ m≤′n)

z≤′n :  {n}  zero ≤′ n
z≤′n {zero}  = ≤′-refl
z≤′n {suc n} = ≤′-step z≤′n

s≤′s :  {m n}  m ≤′ n  suc m ≤′ suc n
s≤′s ≤′-refl        = ≤′-refl
s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)

≤⇒≤′ : _≤_  _≤′_
≤⇒≤′ z≤n       = z≤′n
≤⇒≤′ (s≤s m≤n) = s≤′s (≤⇒≤′ m≤n)

------------------------------------------------------------------------
-- Various order-related properties

≤-steps :  {m n} k  m  n  m  k + n
≤-steps zero    m≤n = m≤n
≤-steps (suc k) m≤n = ≤-step (≤-steps k m≤n)

m≤m+n :  m n  m  m + n
m≤m+n zero    n = z≤n
m≤m+n (suc m) n = s≤s (m≤m+n m n)

m≤′m+n :  m n  m ≤′ m + n
m≤′m+n m n = ≤⇒≤′ (m≤m+n m n)

n≤′m+n :  m n  n ≤′ m + n
n≤′m+n zero    n = ≤′-refl
n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)

n≤m+n :  m n  n  m + n
n≤m+n m n = ≤′⇒≤ (n≤′m+n m n)

n≤1+n :  n  n  1 + n
n≤1+n _ = ≤-step ≤-refl

1+n≰n :  {n}  ¬ 1 + n  n
1+n≰n (s≤s le) = 1+n≰n le

≤pred⇒≤ :  m n  m  pred n  m  n
≤pred⇒≤ m zero    le = le
≤pred⇒≤ m (suc n) le = ≤-step le

≤⇒pred≤ :  m n  m  n  pred m  n
≤⇒pred≤ zero    n le = le
≤⇒pred≤ (suc m) n le = start
  m     ≤⟨ n≤1+n m 
  suc m ≤⟨ le 
  n     

¬i+1+j≤i :  i {j}  ¬ i + suc j  i
¬i+1+j≤i zero    ()
¬i+1+j≤i (suc i) le = ¬i+1+j≤i i (≤-pred le)

n∸m≤n :  m n  n  m  n
n∸m≤n zero    n       = ≤-refl
n∸m≤n (suc m) zero    = ≤-refl
n∸m≤n (suc m) (suc n) = start
  n  m  ≤⟨ n∸m≤n m n 
  n      ≤⟨ n≤1+n n 
  suc n  

n≤m+n∸m :  m n  n  m + (n  m)
n≤m+n∸m m       zero    = z≤n
n≤m+n∸m zero    (suc n) = ≤-refl
n≤m+n∸m (suc m) (suc n) = s≤s (n≤m+n∸m m n)

m⊓n≤m :  m n  m  n  m
m⊓n≤m zero    _       = z≤n
m⊓n≤m (suc m) zero    = z≤n
m⊓n≤m (suc m) (suc n) = s≤s $ m⊓n≤m m n

m≤m⊔n :  m n  m  m  n
m≤m⊔n zero    _       = z≤n
m≤m⊔n (suc m) zero    = ≤-refl
m≤m⊔n (suc m) (suc n) = s≤s $ m≤m⊔n m n

⌈n/2⌉≤′n :  n   n /2⌉ ≤′ n
⌈n/2⌉≤′n zero          = ≤′-refl
⌈n/2⌉≤′n (suc zero)    = ≤′-refl
⌈n/2⌉≤′n (suc (suc n)) = s≤′s (≤′-step (⌈n/2⌉≤′n n))

⌊n/2⌋≤′n :  n   n /2⌋ ≤′ n
⌊n/2⌋≤′n zero    = ≤′-refl
⌊n/2⌋≤′n (suc n) = ≤′-step (⌈n/2⌉≤′n n)

<-trans : Transitive _<_
<-trans {i} {j} {k} i<j j<k = start
  1 + i  ≤⟨ i<j 
  j      ≤⟨ n≤1+n j 
  1 + j  ≤⟨ j<k 
  k      

≰⇒> : _≰_  _>_
≰⇒> {zero}          z≰n with z≰n z≤n
... | ()
≰⇒> {suc m} {zero}  _   = s≤s z≤n
≰⇒> {suc m} {suc n} m≰n = s≤s (≰⇒> (m≰n  s≤s))

------------------------------------------------------------------------
-- (ℕ, _≡_, _<_) is a strict total order

m≢1+m+n :  m {n}  m  suc (m + n)
m≢1+m+n zero    ()
m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record
  { Carrier            = 
  ; _≈_                = _≡_
  ; _<_                = _<_
  ; isStrictTotalOrder = record
    { isEquivalence = PropEq.isEquivalence
    ; trans         = <-trans
    ; compare       = cmp
    ; <-resp-≈      = PropEq.resp₂ _<_
    }
  }
  where
  2+m+n≰m :  {m n}  ¬ 2 + (m + n)  m
  2+m+n≰m (s≤s le) = 2+m+n≰m le

  cmp : Trichotomous _≡_ _<_
  cmp m n with compare m n
  cmp .m .(suc (m + k)) | less    m k = tri< (m≤m+n (suc m) k) (m≢1+m+n _) 2+m+n≰m
  cmp .n             .n | equal   n   = tri≈ 1+n≰n refl 1+n≰n
  cmp .(suc (n + k)) .n | greater n k = tri> 2+m+n≰m (m≢1+m+n _  sym) (m≤m+n (suc n) k)

------------------------------------------------------------------------
-- Miscellaneous other properties

0∸n≡0 : LeftZero zero _∸_
0∸n≡0 zero    = refl
0∸n≡0 (suc _) = refl

n∸n≡0 :  n  n  n  0
n∸n≡0 zero    = refl
n∸n≡0 (suc n) = n∸n≡0 n

∸-+-assoc :  m n o  (m  n)  o  m  (n + o)
∸-+-assoc m       n       zero    = cong (_∸_ m) (sym $ proj₂ +-identity n)
∸-+-assoc zero    zero    (suc o) = refl
∸-+-assoc zero    (suc n) (suc o) = refl
∸-+-assoc (suc m) zero    (suc o) = refl
∸-+-assoc (suc m) (suc n) (suc o) = ∸-+-assoc m n (suc o)

+-∸-assoc :  m {n o}  o  n  (m + n)  o  m + (n  o)
+-∸-assoc m (z≤n {n = n})             = begin m + n 
+-∸-assoc m (s≤s {m = o} {n = n} o≤n) = begin
  (m + suc n)  suc o  ≡⟨ cong  n  n  suc o) (m+1+n≡1+m+n m n) 
  suc (m + n)  suc o  ≡⟨ refl 
  (m + n)  o          ≡⟨ +-∸-assoc m o≤n 
  m + (n  o)          

m+n∸n≡m :  m n  (m + n)  n  m
m+n∸n≡m m n = begin
  (m + n)  n  ≡⟨ +-∸-assoc m (≤-refl {x = n}) 
  m + (n  n)  ≡⟨ cong (_+_ m) (n∸n≡0 n) 
  m + 0        ≡⟨ proj₂ +-identity m 
  m            

m+n∸m≡n :  {m n}  m  n  m + (n  m)  n
m+n∸m≡n {m} {n} m≤n = begin
  m + (n  m)  ≡⟨ sym $ +-∸-assoc m m≤n 
  (m + n)  m  ≡⟨ cong  n  n  m) (+-comm m n) 
  (n + m)  m  ≡⟨ m+n∸n≡m n m 
  n            

m⊓n+n∸m≡n :  m n  (m  n) + (n  m)  n
m⊓n+n∸m≡n zero    n       = refl
m⊓n+n∸m≡n (suc m) zero    = refl
m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n

[m∸n]⊓[n∸m]≡0 :  m n  (m  n)  (n  m)  0
[m∸n]⊓[n∸m]≡0 zero zero       = refl
[m∸n]⊓[n∸m]≡0 zero (suc n)    = refl
[m∸n]⊓[n∸m]≡0 (suc m) zero    = refl
[m∸n]⊓[n∸m]≡0 (suc m) (suc n) = [m∸n]⊓[n∸m]≡0 m n

[i+j]∸[i+k]≡j∸k :  i j k  (i + j)  (i + k)  j  k
[i+j]∸[i+k]≡j∸k zero    j k = refl
[i+j]∸[i+k]≡j∸k (suc i) j k = [i+j]∸[i+k]≡j∸k i j k

-- TODO: Can this proof be simplified? An automatic solver which can
-- handle ∸ would be nice...

i∸k∸j+j∸k≡i+j∸k :  i j k  i  (k  j) + (j  k)  i + j  k
i∸k∸j+j∸k≡i+j∸k zero j k = begin
  0  (k  j) + (j  k)
                         ≡⟨ cong  x  x + (j  k)) (0∸n≡0 (k  j)) 
  0 + (j  k)
                         ≡⟨ refl 
  j  k
                         
i∸k∸j+j∸k≡i+j∸k (suc i) j zero = begin
  suc i  (0  j) + j
                       ≡⟨ cong  x  suc i  x + j) (0∸n≡0 j) 
  suc i  0 + j
                       ≡⟨ refl 
  suc (i + j)
                       
i∸k∸j+j∸k≡i+j∸k (suc i) zero (suc k) = begin
  i  k + 0
             ≡⟨ proj₂ +-identity _ 
  i  k
             ≡⟨ cong  x  x  k) (sym (proj₂ +-identity _)) 
  i + 0  k
             
i∸k∸j+j∸k≡i+j∸k (suc i) (suc j) (suc k) = begin
  suc i  (k  j) + (j  k)
                             ≡⟨ i∸k∸j+j∸k≡i+j∸k (suc i) j k 
  suc i + j  k
                             ≡⟨ cong  x  x  k)
                                     (sym (m+1+n≡1+m+n i j)) 
  i + suc j  k
                             

i+j≡0⇒i≡0 :  i {j}  i + j  0  i  0
i+j≡0⇒i≡0 zero    eq = refl
i+j≡0⇒i≡0 (suc i) ()

i+j≡0⇒j≡0 :  i {j}  i + j  0  j  0
i+j≡0⇒j≡0 i {j} i+j≡0 = i+j≡0⇒i≡0 j $ begin
  j + i
    ≡⟨ +-comm j i 
  i + j
    ≡⟨ i+j≡0 
  0
    

i*j≡0⇒i≡0∨j≡0 :  i {j}  i * j  0  i  0  j  0
i*j≡0⇒i≡0∨j≡0 zero    {j}     eq = inj₁ refl
i*j≡0⇒i≡0∨j≡0 (suc i) {zero}  eq = inj₂ refl
i*j≡0⇒i≡0∨j≡0 (suc i) {suc j} ()

i*j≡1⇒i≡1 :  i j  i * j  1  i  1
i*j≡1⇒i≡1 (suc zero)    j             _  = refl
i*j≡1⇒i≡1 zero          j             ()
i*j≡1⇒i≡1 (suc (suc i)) (suc (suc j)) ()
i*j≡1⇒i≡1 (suc (suc i)) (suc zero)    ()
i*j≡1⇒i≡1 (suc (suc i)) zero          eq with begin
  0      ≡⟨ *-comm 0 i 
  i * 0  ≡⟨ eq 
  1      
... | ()

i*j≡1⇒j≡1 :  i j  i * j  1  j  1
i*j≡1⇒j≡1 i j eq = i*j≡1⇒i≡1 j i (begin
  j * i  ≡⟨ *-comm j i 
  i * j  ≡⟨ eq 
  1      )

cancel-+-left :  i {j k}  i + j  i + k  j  k
cancel-+-left zero    eq = eq
cancel-+-left (suc i) eq = cancel-+-left i (cong pred eq)

cancel-+-left-≤ :  i {j k}  i + j  i + k  j  k
cancel-+-left-≤ zero    le       = le
cancel-+-left-≤ (suc i) (s≤s le) = cancel-+-left-≤ i le

cancel-*-right :  i j {k}  i * suc k  j * suc k  i  j
cancel-*-right zero    zero        eq = refl
cancel-*-right zero    (suc j)     ()
cancel-*-right (suc i) zero        ()
cancel-*-right (suc i) (suc j) {k} eq =
  cong suc (cancel-*-right i j (cancel-+-left (suc k) eq))

cancel-*-right-≤ :  i j k  i * suc k  j * suc k  i  j
cancel-*-right-≤ zero    _       _ _  = z≤n
cancel-*-right-≤ (suc i) zero    _ ()
cancel-*-right-≤ (suc i) (suc j) k le =
  s≤s (cancel-*-right-≤ i j k (cancel-+-left-≤ (suc k) le))

*-distrib-∸ʳ : _*_ DistributesOverʳ _∸_
*-distrib-∸ʳ i zero k = begin
  (0  k) * i  ≡⟨ cong₂ _*_ (0∸n≡0 k) refl 
  0            ≡⟨ sym $ 0∸n≡0 (k * i) 
  0  k * i    
*-distrib-∸ʳ i (suc j) zero    = begin i + j * i 
*-distrib-∸ʳ i (suc j) (suc k) = begin
  (j  k) * i             ≡⟨ *-distrib-∸ʳ i j k 
  j * i  k * i           ≡⟨ sym $ [i+j]∸[i+k]≡j∸k i _ _ 
  i + j * i  (i + k * i) 

im≡jm+n⇒[i∸j]m≡n
  :  i j m n 
    i * m  j * m + n  (i  j) * m  n
im≡jm+n⇒[i∸j]m≡n i j m n eq = begin
  (i  j) * m            ≡⟨ *-distrib-∸ʳ m i j 
  (i * m)  (j * m)      ≡⟨ cong₂ _∸_ eq (refl {x = j * m}) 
  (j * m + n)  (j * m)  ≡⟨ cong₂ _∸_ (+-comm (j * m) n) (refl {x = j * m}) 
  (n + j * m)  (j * m)  ≡⟨ m+n∸n≡m n (j * m) 
  n                      

i+1+j≢i :  i {j}  i + suc j  i
i+1+j≢i i eq = ¬i+1+j≤i i (reflexive eq)
  where open DecTotalOrder decTotalOrder

⌊n/2⌋-mono : ⌊_/2⌋ Preserves _≤_  _≤_
⌊n/2⌋-mono z≤n             = z≤n
⌊n/2⌋-mono (s≤s z≤n)       = z≤n
⌊n/2⌋-mono (s≤s (s≤s m≤n)) = s≤s (⌊n/2⌋-mono m≤n)

⌈n/2⌉-mono : ⌈_/2⌉ Preserves _≤_  _≤_
⌈n/2⌉-mono m≤n = ⌊n/2⌋-mono (s≤s m≤n)

pred-mono : pred Preserves _≤_  _≤_
pred-mono z≤n      = z≤n
pred-mono (s≤s le) = le

_+-mono_ : _+_ Preserves₂ _≤_  _≤_  _≤_
_+-mono_ {zero} {m₂} {n₁} {n₂} z≤n n₁≤n₂ = start
  n₁      ≤⟨ n₁≤n₂ 
  n₂      ≤⟨ n≤m+n m₂ n₂ 
  m₂ + n₂ 
s≤s m₁≤m₂ +-mono n₁≤n₂ = s≤s (m₁≤m₂ +-mono n₁≤n₂)

_*-mono_ : _*_ Preserves₂ _≤_  _≤_  _≤_
z≤n       *-mono n₁≤n₂ = z≤n
s≤s m₁≤m₂ *-mono n₁≤n₂ = n₁≤n₂ +-mono (m₁≤m₂ *-mono n₁≤n₂)

∸-mono : _∸_ Preserves₂ _≤_  _≥_  _≤_
∸-mono           z≤n         (s≤s n₁≥n₂)    = z≤n
∸-mono           (s≤s m₁≤m₂) (s≤s n₁≥n₂)    = ∸-mono m₁≤m₂ n₁≥n₂
∸-mono {m₁} {m₂} m₁≤m₂       (z≤n {n = n₁}) = start
  m₁  n₁  ≤⟨ n∸m≤n n₁ m₁ 
  m₁       ≤⟨ m₁≤m₂ 
  m₂