    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Coprimality
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Integer.Coprimality where

    open import Data.Integer.Base using (ℤ; _*_; ∣_∣)
    open import Data.Integer.Divisibility using (_∣_)
    open import Data.Integer.Properties using (abs-*)
    import Data.Nat.Coprimality as ℕ
      using (Coprime; sym; coprime?; coprime-divisor)
    import Data.Nat.Divisibility as ℕ using (_∣_)
    open import Function.Base using (_on_)
    open import Level using (0ℓ)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Definitions using (Decidable; Symmetric)
    open import Relation.Binary.PropositionalEquality.Core using (subst)

    ------------------------------------------------------------------------
    -- Definition

    Coprime : Rel ℤ 0ℓ
    Coprime = ℕ.Coprime on ∣_∣

    ------------------------------------------------------------------------
    -- Properties of coprimality

    sym : Symmetric Coprime
    sym = ℕ.sym

    coprime? : Decidable Coprime
    coprime? x y = ℕ.coprime? ∣ x ∣ ∣ y ∣

    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-* j k) eq)