Function vstd::arithmetic::div_mod::lemma_remainder

source ·

pub broadcast proof fn lemma_remainder(x: int, d: int)

Expand description

requires

0 <= x,

0 < d,

ensures

0 <= #[trigger] (x - (x / d * d)) < d,

Proof that the difference between a nonnegative integer x and the division of x by a positive integer d multiplied by d is lower bounded (inclusively) by 0 and upper bounded (exclusively) by `d