Function vstd::arithmetic::div_mod::lemma_remainder

source · 
pub broadcast proof fn lemma_remainder(x: int, d: int)
Expand description
requires
0 <= x,
0 < d,
ensures
0 <= #[trigger] (x - (x / d * d)) < d,

Proof that the difference between a nonnegative integer x and the division of x by a positive integer d multiplied by d is lower bounded (inclusively) by 0 and upper bounded (exclusively) by `d