Function vstd::arithmetic::div_mod::lemma_mod_ordering

source · 
pub broadcast proof fn lemma_mod_ordering(x: int, k: int, d: int)
Expand description
requires
1 < d,
0 < k,
ensures
0 < d * k,
x % d <= #[trigger] (x % (d * k)),

Proof that multiplying the divisor by a positive number can’t decrease the remainder. Specifically, because k > 0, we have x % d <= x % (d * k).