vstd::arithmetic::div_mod

Function lemma_div_basics_1

Source 
pub broadcast proof fn lemma_div_basics_1(x: int)
Expand description
ensures
x != 0 as int ==> #[trigger] (0int / x) == 0,

Proof for basic property that 0 divided by x is 0.