Function vstd::arithmetic::div_mod::lemma_basic_div

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

Proof that dividing any non-negative integer by a larger integer produces a quotient of 0