Idris2Doc : Data.Nat.Division

Data.Nat.Division

`Division theorem for (type-level) natural number division`
DivisionTheorem : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZerodenom) -> (0 prf2 : NonZerodenom) -> numer = modNatNZnumerdenomprf1+ (divNatNZnumerdenomprf2*denom)
Totality: total
DivisionTheoremDivMod : (numer : Nat) -> (denom : Nat) -> (0 prf : NonZerodenom) -> numer = snd (divmodNatNZnumerdenomprf) + (fst (divmodNatNZnumerdenomprf) *denom)
Totality: total
DivisionTheoremUniqueness : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZerodenom) -> (q : Nat) -> (r : Nat) -> LTrdenom -> numer = (q*denom) +r -> (divNatNZnumerdenomdenom_nz = q, modNatNZnumerdenomdenom_nz = r)
Totality: total
DivisionTheoremUniquenessDivMod : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZerodenom) -> (q : Nat) -> (r : Nat) -> LTrdenom -> numer = (q*denom) +r -> divmodNatNZnumerdenomdenom_nz = (q, r)
Totality: total
boundModNatNZ : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZerodenom) -> LT (modNatNZnumerdenomdenom_nz) denom
Totality: total
divmodNatNZeqDivMod : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZerodenom) -> (0 prf2 : NonZerodenom) -> (0 prf3 : NonZerodenom) -> divmodNatNZnumerdenomprf1 = (divNatNZnumerdenomprf2, modNatNZnumerdenomprf3)
Totality: total
fstDivmodNatNZeqDiv : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZerodenom) -> (0 prf2 : NonZerodenom) -> fst (divmodNatNZnumerdenomprf1) = divNatNZnumerdenomprf2
Totality: total
sndDivmodNatNZeqMod : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZerodenom) -> (0 prf2 : NonZerodenom) -> snd (divmodNatNZnumerdenomprf1) = modNatNZnumerdenomprf2
Totality: total