Function vstd::arithmetic::div_mod::lemma_div_decreases

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

Proof that dividing an integer by 2 or more results in a quotient that is smaller than the original dividend. Specifically, x / d < x.