Function vstd::arithmetic::div_mod::lemma_small_mod

source · 
pub proof fn lemma_small_mod(x: nat, m: nat)
Expand description
requires
x < m,
0 < m,
ensures
x % m == x,

Proof that a natural number x divided by a larger natural number gives a remainder equal to x. Specifically, because x < m, we know x % m == x.