Function vstd::arithmetic::div_mod::lemma_div_nonincreasing

source · 
pub broadcast proof fn lemma_div_nonincreasing(x: int, d: int)
Expand description
requires
0 <= x,
0 < d,
ensures
#[trigger] (x / d) <= x,

Proof that dividing an integer by 1 or more results in a quotient that is less than or equal to the original dividend. Specifically, x / d <= x.