Function vstd::arithmetic::div_mod::lemma_div_basics_3

source · 
pub broadcast proof fn lemma_div_basics_3(x: int)
Expand description
ensures
x != 0 ==> #[trigger] (x / x) == 1,