Function vstd::arithmetic::div_mod::lemma_mod_division_less_than_divisor

source · 
pub broadcast proof fn lemma_mod_division_less_than_divisor(x: int, m: int)
Expand description
requires
m > 0,
ensures
0 <= #[trigger] (x % m) < m,

Proof that the remainder of any division will be less than the divisor’s value.