Function vstd::arithmetic::div_mod::lemma_remainder_lower
source · pub broadcast proof fn lemma_remainder_lower(x: int, d: int)Expand description
requires
0 <= x,0 < d,x >= #[trigger] (x / d * d),Proof that the division of a nonnegative integer x by a positive
integer d multiplied by d is less than or equal to the value
of x