Function vstd::arithmetic::div_mod::lemma_mod_pos_bound

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

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