Function vstd::arithmetic::div_mod::lemma_mod_twice

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

Proof that performing (x % m) % m gives the same result as simply perfoming x % m.