Function vstd::arithmetic::div_mod::lemma_div_multiples_vanish_fancy

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

Proof that, since 0 <= b < d, we have (d * x + b) / d == x