Function vstd::arithmetic::div_mod::lemma_div_multiples_vanish

source · 
pub broadcast proof fn lemma_div_multiples_vanish(x: int, d: int)
Expand description
requires
0 < d,
ensures
(d * x) / d == x,

Proof that multiplying an integer by a common numerator and denominator results in the original integer. Specifically, (d * x) / d == x.