Function vstd::arithmetic::div_mod::lemma_round_down

source · 
pub broadcast proof fn lemma_round_down(a: int, r: int, d: int)
Expand description
requires
0 < d,
a % d == 0,
0 <= r < d,
ensures
a == d * ((a + r) / d),

Proof that, since a % d == 0 and 0 <= r < d, we can conclude a == d * (a + r) / d