Function vstd::arithmetic::div_mod::lemma_remainder_lower

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

Proof that the division of a nonnegative integer x by a positive integer d multiplied by d is less than or equal to the value of x