Function vstd::arithmetic::div_mod::lemma_mod_multiples_basic

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

Proof that multiplying by a number then dividing by that same number produces a remainder of 0. Specifically, (x * m) % m == 0.