Function vstd::arithmetic::div_mod::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.