Function vstd::arithmetic::div_mod::lemma_mod_is_mod_recursive

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.