open import 1Lab.Prelude

open import Data.Int
open import Data.Nat as Nat

module Data.Int.Divisible where


# Divisibility of integersπ

We define what it means for an integer to be divisible by a natural number, as a straightforward generalisation of the case for natural numbers.

_β£β€_ : Nat β Int β Type
zero  β£β€ y = y β‘ 0
suc x β£β€ y = fibre (_*β€ possuc x) y

infix 7 _β£β€_

β£β€-is-prop : β x y β is-prop (x β£β€ y)
β£β€-is-prop zero y n k = prop!
β£β€-is-prop (suc x) y (n , p) (n' , q) = Ξ£-prop-path! (*β€-injectiver-possuc x n n' (p β sym q))

β£β€-is-truncation : β {x y} β (x β£β€ y) β β₯ fibre (_*β€ pos x) y β₯
β£β€-is-truncation {zero} {y} =
prop-ext!
(Ξ» p β inc (y , *β€-zeror y β sym p))
(rec! Ξ» x p β sym p β *β€-zeror x )
β£β€-is-truncation {suc x} {y} = Equiv.to is-propβequivβ₯-β₯ (β£β€-is-prop (suc x) y)

β£β€βfibre : β {x y} β x β£β€ y β fibre (_*β€ pos x) y
β£β€βfibre {zero} wit  = 0 , sym wit
β£β€βfibre {suc x} wit = wit

fibreββ£β€ : β {x y} β fibre (_*β€ pos x) y β x β£β€ y
fibreββ£β€ f = Equiv.from β£β€-is-truncation (inc f)

dividesβ€ : β {x y} (q : Int) β q *β€ pos x β‘ y β x β£β€ y
dividesβ€ x p = fibreββ£β€ (x , p)

β£β€-zero : β {x} β x β£β€ 0
β£β€-zero = dividesβ€ 0 refl

β£β€-one : β {x} β 1 β£β€ x
β£β€-one {x} = dividesβ€ x (*β€-oner x)

mβ£β€snβmβ€sn : β {x y} β Β¬ (y β‘ 0) β x β£β€ y β x Nat.β€ abs y
mβ£β€snβmβ€sn {x} {y} nz p with β£β€βfibre p
... | posz , p = absurd (nz (sym p))
... | possuc k , p = differenceββ€ (k * x)
(ap abs (sym (assign-pos (x + k * x))) β ap abs p)
... | negsuc k , p = differenceββ€ (k * x)
(sym (abs-negβ€ (pos (x + k * x))) β ap abs (sym (assign-neg (x + k * x))) β ap abs p)

β£β€-+ : β {k n m} β k β£β€ n β k β£β€ m β k β£β€ (n +β€ m)
β£β€-+ {zero} {n} {m} p q = apβ _+β€_ p q
β£β€-+ {suc k} (x , p) (y , q) = x +β€ y , *β€-distribr (possuc k) x y β apβ _+β€_ p q

β£β€-negβ€ : β {k n} β k β£β€ n β k β£β€ negβ€ n
β£β€-negβ€ {zero} d = ap negβ€ d
β£β€-negβ€ {suc k} (x , p) = negβ€ x , *β€-negl x _ β ap negβ€ p