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