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,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.