Function vstd::arithmetic::div_mod::lemma_mod_decreases

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

Proof that when natural number x is divided by natural number m, the remainder will be less than or equal to x.