let Nat =
      https://prelude.dhall-lang.org/v21.1.0/Natural/package.dhall
        sha256:ee9ed2b28a417ed4e9a0c284801b928bf91b3fbdc1a68616347678c1821f1ddf

let Int =
      https://prelude.dhall-lang.org/v21.1.0/Integer/package.dhall
        sha256:d1a572ca3a764781496847e4921d7d9a881c18ffcfac6ae28d0e5299066938a0

let foldWhile
    : forall (n : Natural) ->
      forall (res : Type) ->
      forall (succ : res -> Optional res) ->
      forall (zero : res) ->
        res
    = \(n : Natural) ->
      \(R : Type) ->
      \(succ : R -> Optional R) ->
      \(zero : R) ->
        let Acc
            : Type
            = { current : R, done : Bool }

        let update
            : Acc -> Acc
            = \(acc : Acc) ->
                if    acc.done
                then  acc
                else  merge
                        { Some = \(r : R) -> acc // { current = r }
                        , None = acc // { done = True }
                        }
                        (succ acc.current)

        let init
            : Acc
            = { current = zero, done = False }

        let result
            : Acc
            = Natural/fold n Acc update init

        in  result.current

let DivRes = \(a : Type) -> { remainder : a, quotiant : a }

let QED = assert : True === True

let downwardSteps =
      \(x : Natural) ->
      \(y : Natural) ->
        let initAcc
            : DivRes Natural
            = { remainder = x, quotiant = 0 }

        let updateAcc
            : DivRes Natural -> Optional (DivRes Natural)
            = \(acc : DivRes Natural) ->
                if    Nat.lessThan acc.remainder y
                then  None (DivRes Natural)
                else  Some
                        { remainder = Natural/subtract y acc.remainder
                        , quotiant = acc.quotiant + 1
                        }

        in  foldWhile (x + 1) (DivRes Natural) updateAcc initAcc

let Natural/quotRemUnsafe
    : forall (a : Natural) -> Natural -> DivRes Natural
    = \(x : Natural) -> \(y : Natural) -> downwardSteps y x

let Natural/quotRem
    : forall (a : Natural) ->
      Nat.isZero a == False === True ->
      Natural ->
        DivRes Natural
    = \(x : Natural) ->
      \(_ : Nat.isZero x == False === True) ->
      \(y : Natural) ->
        Natural/quotRemUnsafe x y

let Natural/div
    : forall (a : Natural) ->
      Nat.isZero a == False === True ->
      Natural ->
        Natural
    = \(x : Natural) ->
      \(a : Nat.isZero x == False === True) ->
      \(y : Natural) ->
        (Natural/quotRem x a y).quotiant

let d1 = assert : Natural/div 1 QED 1 === 1

let d2 = assert : Natural/div 2 QED 1 === 0

let d3 = assert : Natural/div 2 QED 5 === 2

let Natural/rem
    : forall (a : Natural) ->
      Nat.isZero a == False === True ->
      Natural ->
        Natural
    = \(x : Natural) ->
      \(a : Nat.isZero x == False === True) ->
      \(y : Natural) ->
        (Natural/quotRem x a y).remainder

let r1 = assert : Natural/rem 2 QED 4 === 0

let r2 = assert : Natural/rem 2 QED 5 === 1

let Natural/pow
    : Natural -> Natural -> Natural
    = \(b : Natural) ->
      \(p : Natural) ->
        Natural/fold p Natural (\(x : Natural) -> x * b) 1

let p1 = assert : Natural/pow 10 1 === 10

let p2 = assert : Natural/pow 10 3 === 1000

let p3 = assert : Natural/pow 10 0 === 1

let Integer/quotRemUnsafe
    : Natural -> Integer -> DivRes Integer
    = \(x : Natural) ->
      \(y : Integer) ->
        if    Int.equal y +0
        then  { quotiant = +0, remainder = +0 }
        else  let sign = if Int.positive y then +1 else -1

              let toInt = \(x : Natural) -> Int.multiply sign (Nat.toInteger x)

              let res = Natural/quotRemUnsafe x (Int.abs y)

              in  { quotiant = toInt res.quotiant
                  , remainder = toInt res.remainder
                  }

let Integer/quotRem
    : forall (a : Natural) ->
      Nat.isZero a == False === True ->
      Integer ->
        DivRes Integer
    = \(x : Natural) ->
      \(_ : Nat.isZero x == False === True) ->
      \(y : Integer) ->
        Integer/quotRemUnsafe x y

let Integer/div
    : forall (a : Natural) ->
      Nat.isZero a == False === True ->
      Integer ->
        Integer
    = \(x : Natural) ->
      \(a : Nat.isZero x == False === True) ->
      \(y : Integer) ->
        (Integer/quotRem x a y).quotiant

let id1 = assert : Integer/div 1 QED +3 === +3

let id2 = assert : Integer/div 1 QED -3 === -3

let id3 = assert : Integer/div 2 QED -7 === -3

let Integer/rem
    : forall (a : Natural) ->
      Nat.isZero a == False === True ->
      Integer ->
        Integer
    = \(x : Natural) ->
      \(a : Nat.isZero x == False === True) ->
      \(y : Integer) ->
        (Integer/quotRem x a y).remainder

let ir1 = assert : Integer/rem 1 QED +3 === +0

let ir2 = assert : Integer/rem 1 QED -3 === -0

let ir3 = assert : Integer/rem 2 QED -7 === -1

in  { QED
    , DivRes
    , Natural/div
    , Natural/rem
    , Natural/quotRem
    , Natural/quotRemUnsafe
    , Natural/pow
    , Integer/quotRem
    , Integer/quotRemUnsafe
    , Integer/div
    , Integer/rem
    }