Function vstd::arithmetic::div_mod::lemma_mod_is_mod_recursive
source · pub broadcast proof fn lemma_mod_is_mod_recursive(x: int, m: int)Expand description
requires
m > 0,mod_recursive(x, m) == #[trigger] (x % m),Proof that computing the modulus using % is equivalent to
computing it with a recursive definition of modulus. Specifically,
x % m is equivalent in that way.