vstd::arithmetic::div_mod

Function lemma_div_basics_5

Source
pub broadcast proof fn lemma_div_basics_5(x: int, y: int)
Expand description
ensures
x >= 0 && y > 0 ==> #[trigger] (x / y) <= x,

Proof that the quotient produced by dividing any non-negative integer x by a positive integer y is at most x.