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.