Function vstd::arithmetic::div_mod::lemma_basic_div_specific_divisor

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

Proof that dividing any non-negative integer less than d by d produces a quotient of 0