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.