Idris2Doc : Data.Nat.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