Function vstd::arithmetic::div_mod::lemma_fundamental_div_mod_converse_mod

source · 
pub broadcast proof fn lemma_fundamental_div_mod_converse_mod(x: int, d: int, q: int, r: int)
Expand description
requires
d != 0,
0 <= r < d,
x == #[trigger] (q * d + r),
ensures
r == #[trigger] (x % d),

Proof of the converse of the fundamental property of division and modulo. Specifically, if we know 0 <= r < d and x == q * d + r, then we know that r is the remainder x % d.