```module Data.ForeignNat.Divisibility where

open import Data.ForeignNat

open import Data.Bool using (Bool; true; false)
open import Relation.Binary.Core
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Nat
open import Data.Nat.Divisibility
open import Relation.Binary.PropositionalEquality
open import Data.Product

open import Algebra
import Data.Nat.Properties as Nat
private
module ℕ = CommutativeSemiring Nat.commutativeSemiring

{-# IMPORT Data.ForeignNat.Impl #-}

postulate
_/′_ : ℕ′ → ℕ′ → ℕ′
_%′_ : ℕ′ → ℕ′ → ℕ′

muldiv : ∀ {m n q r} → (q ≡ unmarshalℕ ((marshalℕ n) /′ (marshalℕ m))) → (r ≡ unmarshalℕ ((marshalℕ n) %′ (marshalℕ m))) → n ≡ q * m + r
∣-%-consistency : ∀ {m n} → m ∣ n → (marshalℕ n %′ marshalℕ m) ≡ zero

{-# COMPILED _/′_ Data.ForeignNat.Impl.divide #-}
{-# COMPILED _%′_ Data.ForeignNat.Impl.modulo #-}

_∣?′_ : Decidable _∣_
m ∣?′ n with ((marshalℕ n) %′ (marshalℕ m)) ≟′ zero
...    | yes noRem with muldiv refl (cong unmarshalℕ (sym noRem))
...                | n=q*m+0 = yes (divides q n=q*m)
where q = unmarshalℕ ((marshalℕ n) /′ (marshalℕ m))
n=q*m = begin
n
≡⟨ n=q*m+0 ⟩
q * m + 0
≡⟨ proj₂ ℕ.+-identity (q * m) ⟩
q * m
∎ where open ≡-Reasoning
m ∣?′ n | no rem = no λ m∣n → contradiction (∣-%-consistency m∣n) rem
```