Idris2Doc : Data.Nat.Division

Data.Nat.Division

Division theorem for (type-level) natural number division

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
DivisionTheoremDivMod : (numer : Nat) -> (denom : Nat) -> (0 prf : NonZero denom) -> numer = snd (divmodNatNZ numer denom prf) + (fst (divmodNatNZ numer denom prf) * denom): Totality: total
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
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
boundModNatNZ : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom) -> LT (modNatNZ numer denom denom_nz) denom: Totality: total
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
fstDivmodNatNZeqDiv : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZero denom) -> (0 prf2 : NonZero denom) -> fst (divmodNatNZ numer denom prf1) = divNatNZ numer denom prf2: Totality: total
sndDivmodNatNZeqMod : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZero denom) -> (0 prf2 : NonZero denom) -> snd (divmodNatNZ numer denom prf1) = modNatNZ numer denom prf2: Totality: total