Function vstd::arithmetic::div_mod::lemma_div_pos_is_pos

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

Proof that dividing a whole number by a natural number will result in a quotient that is greater than or equal to 0. Specifically, x / d >= 0.