Function vstd::arithmetic::div_mod::lemma_fundamental_div_mod_converse_div
source · pub broadcast proof fn lemma_fundamental_div_mod_converse_div(x: int, d: int, q: int, r: int)Expand description
requires
d != 0,0 <= r < d,x == #[trigger] (q * d + r),q == #[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 q is the quotient x / d.