Function vstd::arithmetic::div_mod::lemma_multiply_divide_le
source · pub broadcast proof fn lemma_multiply_divide_le(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 or equal to the product of
two other integers, then the quotient with one of them will be
less than or equal to the other of them. Specifically, because
a <= b * c, we know a / b <= c.