module My.SetTheory.Nat.Divisibility where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Algebra as A
import Data.Empty as DE
import Data.Nat as DN
import Data.Nat.Divisibility as DND
import Data.Nat.Properties as DNP
import Data.Sum as DS
import Function as F
import Relation.Binary as RB
import Relation.Binary.PropositionalEquality as RBPE

open DN using (_*_ ; _≤_ ; _<_)
open DND using (_∣_)
open DS using (_⊎_)
open F using (_$_)
open RBPE using (_≡_ ; _≢_)

import My.SetTheory.Nat.Order as MySTNO
import My.SetTheory.Nat.TvD as MySTNTVD
import My.SetTheory.Sum.Misc as MySTSM

-- §──────────────────────────────────────────────────────────────────
-- Basic properties
-- §──────────────────────────────────────────────────────────────────

quotientEqn : {m n : DN.ℕ} → (m∣n : m ∣ n) → n ≡ (DND.quotient m∣n) * m
quotientEqn (DND.divides q n≡q*m) = n≡q*m

-- §──────────────────────────────────────────────────────────────────
-- Any nat divisible by 0 must be 0.
-- §──────────────────────────────────────────────────────────────────

0∣n⇒n≡0 : {n : DN.ℕ} →  ∣ n → n ≡ 
0∣n⇒n≡0 {n} (DND.divides q n≡q*0) =
  begin
    n     ≡⟨ n≡q*0 ⟩
    q *  ≡⟨ CSR.*-comm q  ⟩
     * q ≡⟨⟩
         ∎
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring
    open RBPE.≡-Reasoning

-- §──────────────────────────────────────────────────────────────────
-- If m divides a positive integer, then m is positive.
-- §──────────────────────────────────────────────────────────────────

1≤n⇒m∣n⇒m≢0 : {m n : DN.ℕ} →  ≤ n → m ∣ n → m ≢ 
1≤n⇒m∣n⇒m≢0 {m} {n} 1≤n m∣n m≡0 = r
  where
    0≡m :  ≡ m
    0≡m = RBPE.sym m≡0
    0∣m :  ∣ m
    0∣m = DIV.reflexive 0≡m
      where
        module DIV = RB.Poset DND.poset
    0∣n :  ∣ n
    0∣n = DIV.trans 0∣m m∣n
      where
        module DIV = RB.Poset DND.poset
    n≡0 : n ≡ 
    n≡0 = 0∣n⇒n≡0 0∣n
    n≢0 : n ≢ 
    n≢0 = MySTNO.1≤n⇒n≢0 1≤n
    r   : DE.⊥
    r   = n≢0 n≡0

1≤n⇒m|n⇒0<m : {m n : DN.ℕ} →  ≤ n → m ∣ n →  < m
1≤n⇒m|n⇒0<m {m} {n} 1≤n m∣n = 0<m
  where
    m≢0     : m ≢ 
    m≢0     = 1≤n⇒m∣n⇒m≢0 1≤n m∣n
    0≢m     :  ≢ m
    0≢m 0≡m = m≢0 $ RBPE.sym 0≡m
    0≤m     :  ≤ m
    0≤m     = DN.z≤n
    0<m⊎0≡m :  < m ⊎  ≡ m
    0<m⊎0≡m = MySTNTVD.m≤n⇒m<n⊎m≡n 0≤m
    0<m     :  < m
    0<m     = MySTSM.¬B⇒A⊎B⇒A 0≢m 0<m⊎0≡m