-- Divides relation on ints

-- Divides relation on nats

```

-- Because if one of the implicit arguments (`m` or `n`) is zero, it cannot be greater than anything else that's non-zero
≤-antisym' : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym' z≤n       z≤n        =  refl
≤-antisym' (s≤s m≤n) (s≤s n≤m)  =  cong suc (≤-antisym m≤n n≤m)
-- The case for the constructor s≤s is impossible
-- because unification ended with a conflicting equation
--   suc n ≟ zero
-- Possible solution: remove the clause, or use an absurd pattern ().
-- when checking that the pattern s≤s n≤m has type n ≤ zero
-- ≤-antisym' z≤n (s≤s n≤m)        =  ?
-- ≤-antisym' (s≤s n≤m) z≤n        =  ?

```

*-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
  → n * p ≤ n * q
*-monoʳ-≤ zero p q p≤q = z≤n
-- Goal: p + n * p ≤ q + n * q
*-monoʳ-≤ (suc n) p q p≤q =
  let n*p≤n*q = (*-monoʳ-≤ n p q p≤q) in
  +-mono-≤ p q (n * p) (n * q) p≤q n*p≤n*q
*-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
  → m * p ≤ n * p
*-monoˡ-≤ m n p m≤n rewrite *-comm m p | *-comm n p = *-monoʳ-≤ p m n m≤n
*-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
  → m * p ≤ n * q
*-mono-≤ m n p q m≤n p≤q = ≤-trans (*-monoˡ-≤ m n p m≤n) (*-monoʳ-≤ n p q p≤q)

<-trans : ∀ {m n p : ℕ}
  → m < n
  → n < p
  → m < p
<-trans z<s (s<s n<p) = z<s
<-trans (s<s m<n) (s<s n<p) = s<s (<-trans m<n n<p)

infix 4 _>_
-- NOTE: This does not work as it has incomplete cases
-- _>_ : ∀ {m n : ℕ} → n < m
-- _>_ {suc m} {zero} = z<s
-- _>_ {suc m} {suc n} = s<s {n} {m} (_>_ {m} {n})
-- NOTE: no relation to `_<_`
data _>_ : ℕ → ℕ → Set where
  s>z : ∀ {n : ℕ} → suc n > zero
  s>s : ∀ {m n : ℕ} → m > n → suc m > suc n
data Trichotomy (m n : ℕ) : Set where
  forward : m > n → Trichotomy m n
  flipped : n > m → Trichotomy m n
  equal   : m ≡ n → Trichotomy m n
-- NOTE: relation to `_<_`, but seems complicated
-- data _>_ : ∀ {m n : ℕ} {n<m : n < m} → Set where
--   s>z : ∀ {m : ℕ} → _>_ {suc m} {zero} {z<s}
--   s>s : ∀ {m n : ℕ} → (n<m : n < m) → _>_ {suc m} {suc n} {s<s n<m}
-- data Trichotomy (m n : ℕ) : Set where
--   forward : (n<m : n < m) → _>_ {m} {n} {n<m} → Trichotomy m n
--   flipped : (m<n : m < n) → _>_ {n} {m} {m<n} → Trichotomy m n
--   equal   : m ≡ n → Trichotomy m n

+-monoʳ-< : ∀ (n p q : ℕ)
  → p < q
  → n + p < n + q
+-monoʳ-< zero p q p<q = p<q
+-monoʳ-< (suc n) p q p<q = s<s (+-monoʳ-< n p q p<q)
+-monoˡ-< : ∀ (m n p : ℕ)
  → m < n
  → m + p < n + p
+-monoˡ-< m n p m<n rewrite +-comm m p | +-comm n p = +-monoʳ-< p m n m<n
+-mono-< : ∀ (m n p q : ℕ)
  → m < n
  → p < q
  → m + p < n + q
+-mono-< m n p q m<n p<q = <-trans (+-monoˡ-< m n p m<n) (+-monoʳ-< n p q p<q)

-- -- NOTE: This doesn't work!
-- -- Case splitting on both m and n seemed to give me absurd cases like the one below.
-- -- The choice of what to match on is very important
-- suc-inv-mono-≤ : ∀ (m n : ℕ) → suc (suc m) ≤ suc n → suc m ≤ n
-- suc-inv-mono-≤ zero zero suc-suc-≤-suc = {!!}
-- suc-inv-mono-≤ zero (suc n) suc-suc-≤-suc = {!!}
-- suc-inv-mono-≤ (suc m) n suc-suc-≤-suc = {!!}
-- -- NOTE: This works, but it's unnecessary as we can match on the proof directly in ≤→<
-- suc-inv-mono-≤ : ∀ (m n : ℕ) → suc (suc m) ≤ suc n → suc m ≤ n
-- suc-inv-mono-≤ m n (s≤s x) = x
≤→< : ∀ (m n : ℕ) → suc m ≤ n → m < n
≤→< zero (suc n) suc-m≤n = z<s
-- NOTE: This was a dead end - I only had to pattern match on the proof
-- ≤→< (suc m) (suc n) suc-m≤n = s<s (≤→< m n (suc-inv-mono-≤ m n suc-m≤n))
≤→< (suc m) (suc n) (s≤s suc-m≤n) = s<s (≤→< m n suc-m≤n)
<→≤ : ∀ {m n : ℕ} → m < n → suc m ≤ n
<→≤ z<s = s≤s z≤n
<→≤ {suc m} {suc n} (s<s m<n) = s≤s (<→≤ m<n)

suc-suc≤→suc≤ : ∀ {m n : ℕ} → suc (suc m) ≤ n → suc m ≤ n
suc-suc≤→suc≤ {zero} {suc n} suc-suc≤ = s≤s z≤n
suc-suc≤→suc≤ {suc m} {suc n} (s≤s suc-suc≤) = s≤s (suc-suc≤→suc≤ suc-suc≤)
<-trans-revisited : ∀ (m n p : ℕ)
  → m < n
  → n < p
  → m < p
<-trans-revisited m n p m<n n<p =
  let suc-suc≤ = (≤-trans (s≤s (<→≤ m<n)) (<→≤ n<p))
  in ≤→< _ _ (suc-suc≤→suc≤ suc-suc≤)

o+o≡e : ∀ {m n : ℕ}
  → odd m
  → odd n
  → even (m + n)
o+o≡e (suc zero) (suc n) = suc (suc n)
o+o≡e (suc (suc m)) (suc n) = suc (suc (o+o≡e m (suc n)))

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (rest O) = rest I
inc (rest I) = (inc rest) O
to   : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)
from : Bin → ℕ
from ⟨⟩ = 0
from (rest O) = 2 * (from rest)
from (rest I) = 1 + 2 * (from rest)
-- Also need to show that inc is canonical as in `inc-can`
data One : Bin -> Set where
  one : One (⟨⟩ I)
  suc : ∀ {b : Bin} → One b → One (inc b)
-- NOTE: Using a bin-law from Induction.lagda.md
from-inc-suc-from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from-inc-suc-from ⟨⟩ = refl
from-inc-suc-from (b O) = refl
from-inc-suc-from (b I) rewrite cong (\x → 2 * x) (from-inc-suc-from b) | *-comm 2 (1 + (from b)) | cong (\x → 2 + x) (*-comm (from b) 2) = refl
1≤from-one : ∀ {b : Bin} → One b → 1 ≤ from b
1≤from-one one = s≤s z≤n
1≤from-one (suc {b} x) rewrite from-inc-suc-from b = s≤s z≤n
data Can : Bin → Set where
  zeroᴮ : Can (⟨⟩ O)
  leading : ∀ {b : Bin} → One b → Can b
inc-can : ∀ {b : Bin} → Can b → Can (inc b)
inc-can zeroᴮ = leading one
inc-can (leading x) = leading (suc x)
to-can : (n : ℕ) → Can (to n)
to-can zero = zeroᴮ
to-can (suc n) = inc-can (to-can n)