Function vstd::arithmetic::div_mod::lemma_div_plus_one

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

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