vstd::arithmetic::div_mod

Function 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,
ensures
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.