------------------------------------------------------------------------
-- The Agda standard library
--
-- Divisibility and coprimality
------------------------------------------------------------------------

module Data.Integer.Divisibility where

open import Function
open import Data.Integer
open import Data.Integer.Properties
import Data.Nat.Divisibility as 
import Data.Nat.Coprimality as 
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

-- Divisibility.

infix 4 _∣_

_∣_ : Rel  zero
_∣_ = ._∣_ on ∣_∣

-- Coprimality.

Coprime : Rel  zero
Coprime = .Coprime on ∣_∣

-- If i divides jk and is coprime to j, then it divides k.

coprime-divisor :  i j k  Coprime i j  i  j * k  i  k
coprime-divisor i j k c eq =
  .coprime-divisor c (subst (._∣_  i ) (abs-*-commute j k) eq)