vstd::arithmetic::div_mod

Function lemma_mod_self_0

Source 
pub broadcast proof fn lemma_mod_self_0(m: int)
Expand description
requires
m > 0,
ensures
#[trigger] (m % m) == 0,

Proof that any integer divided by itself produces a remainder of 0.