vstd::arithmetic::div_mod

Function lemma_div_of0

Source 
pub proof fn lemma_div_of0(d: int)
Expand description
requires
d != 0,
ensures
0 as int / d == 0,

Proof that 0 divided by a nonzero integer is 0, specifically 0 / d == 0.