Data.Nat

Extra utilities for working with Nats

minusLT' : (x : Nat) -> (y : Nat) -> LT' (x - y) (S x)

Subtraction gives a result that is actually smaller.

lteToLt' : LTE (S n) m -> LT' n m

If n + 1 < m, then n < m

ltToLTE : LT' n m -> LTE (S n) m

Convert from LT' to LTE

ltSuccSucc : LT' n m -> LT' (S n) (S m)

If n < m, then 1 + n < 1 + m

divMod : (dividend : Nat) -> (divisor : Nat) -> {auto nonzero : So (not (decAsBool (decEq divisor 0)))} -> DivMod dividend divisor

Division and modulus on Nat, inspired by the definition in the
Agda standard library.

This uses well-founded recursion on LT'.

dividend

the dividend

divisor

the divisor

nonzero

division by zero is nonsense

LTZeroLeast : LT' 0 (S n)

Zero is less than any non-zero number.

data LT' : (n : Nat) -> (m : Nat) -> Type

A strict less-than relation on Nat.

n

the smaller number

m

the larger number

LTSucc : LT' n (S n)

n < 1 + n

LTStep : LT' n m -> LT' n (S m)

n < m implies that n < m + 1

data DivMod : (dividend : Nat) -> (divisor : Nat) -> Type

The result of division on natural numbers.

dividend

the dividend

divisor

the divisor

DivModRes : (quotient : Nat) -> (remainder : Fin divisor) -> (ok : dividend = plus (finToNat remainder) (mult quotient divisor)) -> DivMod dividend divisor

The result of division, with a quotient and a remainder.

dividend

the dividend

divisor

the divisor

quotient

the quotient

remainder

the remainder (bounded by the divisor)

ok

the fact that this is, in fact, a result of division