vstd::arithmetic::div_mod

Function lemma_mod_is_zero

Source 
pub broadcast proof fn lemma_mod_is_zero(x: nat, m: nat)
Expand description
requires
x > 0 && m > 0,
#[trigger] (x % m) == 0,
ensures
x >= m,

Proof that if x % m is zero and x is positive, then x >= m.