Function vstd::arithmetic::div_mod::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