Function vstd::arithmetic::div_mod::lemma_fundamental_div_mod

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

Proof of the fundamental theorem of division and modulo, namely that x can be expressed as d times the quotient x / d plus the remainder x % d.