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