Function vstd::arithmetic::div_mod::lemma_remainder_upper

source · 
pub broadcast proof fn lemma_remainder_upper(x: int, d: int)
Expand description
requires
0 <= x,
0 < d,
ensures
x - d < x / d * d,

Proof that the difference between a nonnegative integer x and a positive integer d must be strictly less than the quotient of x divided by d and then multiplied by d