Function vstd::arithmetic::div_mod::lemma_hoist_over_denominator

source · 
pub broadcast proof fn lemma_hoist_over_denominator(x: int, j: int, d: nat)
Expand description
requires
0 < d,
ensures
x / d as int + j == (x + j * d) / d as int,

Proof that adding an integer to a fraction is equivalent to adding that integer times the denominator to the numerator. Specifically, x / d + j == (x + j * d) / d.