Function vstd::arithmetic::div_mod::lemma_multiply_divide_lt
source · pub broadcast proof fn lemma_multiply_divide_lt(a: int, b: int, c: int)Expand description
requires
0 < b,a < b * c,a / b < c,Proof that if an integer is less than the product of two other
integers, then the quotient with one of them will be less than the
other. Specifically, because a < b * c, we know a / b < c.