Idris2Doc : Data.Nat.Division

# Data.Nat.Division

```Division theorem for (type-level) natural number division
```

## Definitions

`divmodNatNZeqDivMod : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZero denom) -> (0 prf2 : NonZero denom) -> (0 prf3 : NonZero denom) -> divmodNatNZ numer denom prf1 = (divNatNZ numer denom prf2, modNatNZ numer denom prf3)`
Totality: total
Visibility: export
`fstDivmodNatNZeqDiv : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZero denom) -> (0 prf2 : NonZero denom) -> fst (divmodNatNZ numer denom prf1) = divNatNZ numer denom prf2`
Totality: total
Visibility: export
`sndDivmodNatNZeqMod : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZero denom) -> (0 prf2 : NonZero denom) -> snd (divmodNatNZ numer denom prf1) = modNatNZ numer denom prf2`
Totality: total
Visibility: export
`boundModNatNZ : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom) -> LT (modNatNZ numer denom denom_nz) denom`
Totality: total
Visibility: export
`DivisionTheoremDivMod : (numer : Nat) -> (denom : Nat) -> (0 prf : NonZero denom) -> numer = snd (divmodNatNZ numer denom prf) + (fst (divmodNatNZ numer denom prf) * denom)`
Totality: total
Visibility: export
`DivisionTheorem : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZero denom) -> (0 prf2 : NonZero denom) -> numer = modNatNZ numer denom prf1 + (divNatNZ numer denom prf2 * denom)`
Totality: total
Visibility: export
`DivisionTheoremUniquenessDivMod : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom) -> (q : Nat) -> (r : Nat) -> LT r denom -> numer = (q * denom) + r -> divmodNatNZ numer denom denom_nz = (q, r)`
Totality: total
Visibility: export
`DivisionTheoremUniqueness : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom) -> (q : Nat) -> (r : Nat) -> LT r denom -> numer = (q * denom) + r -> (divNatNZ numer denom denom_nz = q, modNatNZ numer denom denom_nz = r)`
Totality: total
Visibility: export
`modDividendMinusDivMultDivider : (0 numer : Nat) -> (0 denom : Nat) -> {auto 0 denom_nz : NonZero denom} -> modNatNZ numer denom denom_nz = minus numer (divNatNZ numer denom denom_nz * denom)`
Totality: total
Visibility: export