Function vstd::arithmetic::div_mod::lemma_fundamental_div_mod_converse

source ·

pub proof fn lemma_fundamental_div_mod_converse(x: int, d: int, q: int, r: int)

Expand description

requires

d != 0,

0 <= r < d,

x == q * d + r,

ensures

r == x % d,

q == 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 and r is the remainder x % d.