Module vstd::arithmetic::div_mod
source · 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 *******************************************************************************/