Function vstd::arithmetic::div_mod::lemma_remainder_upper
source · pub broadcast proof fn lemma_remainder_upper(x: int, d: int)Expand description
requires
0 <= x,0 < d,x - d < x / d * d,Proof that the difference between a nonnegative integer x and a
positive integer d must be strictly less than the quotient of
x divided by d and then multiplied by d