Function vstd::arithmetic::div_mod::lemma_div_basics_4
source · pub broadcast proof fn lemma_div_basics_4(x: int, y: int)Expand description
ensures
x >= 0 && y > 0 ==> #[trigger] (x / y) >= 0,