Function vstd::arithmetic::div_mod::lemma_mod_bound

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

Proof that when integer x is divided by positive integer m, the remainder is nonegative and less than m.