vstd::arithmetic::div_mod

Function lemma_div_minus_one

Source 
pub broadcast proof fn lemma_div_minus_one(x: int, d: int)
Expand description
requires
0 < d,
ensures
-1 + x / d == (-d + x) / d,

Proof that dividing a number then subtracting 1 gives the same result as subtracting the divisor and then doing the division. Specifically, -1 + (x / d) is equal to (-d + x) / d.