Expand description
This file contains proofs related to integer division (/) and
remainder aka mod (%). These are part of the math standard library.
It’s based on the following file from the Dafny math standard
library:
Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy.
That file has the following copyright notice:
/*******************************************************************************
- Original: Copyright (c) Microsoft Corporation * SPDX-License-Identifier: MIT * * Modifications and Extensions: Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/
Functions§
- group_
div_ basics - group_
fundamental_ div_ mod_ converse - group_
mod_ basics - group_
mod_ properties - is_
mod_ equivalent - lemma_
add_ mod_ noop - lemma_
add_ mod_ noop_ right - lemma_
basic_ div - lemma_
basic_ div_ specific_ divisor - lemma_
breakdown - lemma_
div_ basics - lemma_
div_ basics_ 1 - lemma_
div_ basics_ 2 - lemma_
div_ basics_ 3 - lemma_
div_ basics_ 4 - lemma_
div_ basics_ 5 - lemma_
div_ by_ multiple - lemma_
div_ by_ multiple_ is_ strongly_ ordered - lemma_
div_ by_ self - lemma_
div_ decreases - lemma_
div_ denominator - lemma_
div_ is_ div_ recursive - lemma_
div_ is_ ordered - lemma_
div_ is_ ordered_ by_ denominator - lemma_
div_ is_ strictly_ smaller - lemma_
div_ minus_ one - lemma_
div_ multiples_ vanish - lemma_
div_ multiples_ vanish_ fancy - lemma_
div_ multiples_ vanish_ quotient - lemma_
div_ non_ zero - lemma_
div_ nonincreasing - lemma_
div_ of0 - lemma_
div_ plus_ one - lemma_
div_ pos_ is_ pos - lemma_
dividing_ sums - lemma_
fundamental_ div_ mod - lemma_
fundamental_ div_ mod_ converse - lemma_
fundamental_ div_ mod_ converse_ div - lemma_
fundamental_ div_ mod_ converse_ mod - lemma_
hoist_ over_ denominator - lemma_
indistinguishable_ quotients - lemma_
mod_ add_ multiples_ vanish - lemma_
mod_ adds - lemma_
mod_ bound - lemma_
mod_ breakdown - lemma_
mod_ decreases - lemma_
mod_ division_ less_ than_ divisor - lemma_
mod_ equivalence - lemma_
mod_ is_ mod_ recursive - lemma_
mod_ is_ zero - lemma_
mod_ mod - lemma_
mod_ mul_ equivalent - lemma_
mod_ multiples_ basic - lemma_
mod_ multiples_ vanish - lemma_
mod_ neg_ neg - lemma_
mod_ ordering - lemma_
mod_ pos_ bound - lemma_
mod_ self_ 0 - lemma_
mod_ sub_ multiples_ vanish - lemma_
mod_ subtraction - lemma_
mod_ twice - lemma_
mul_ hoist_ inequality - lemma_
mul_ mod_ noop - lemma_
mul_ mod_ noop_ general - lemma_
mul_ mod_ noop_ left - lemma_
mul_ mod_ noop_ right - lemma_
multiply_ divide_ le - lemma_
multiply_ divide_ lt - lemma_
part_ bound1 - lemma_
part_ bound2 - lemma_
remainder - lemma_
remainder_ lower - lemma_
remainder_ upper - lemma_
round_ down - lemma_
small_ div_ converse - lemma_
small_ mod - lemma_
sub_ mod_ noop - lemma_
sub_ mod_ noop_ right - lemma_
truncate_ middle