Function vstd::arithmetic::div_mod::lemma_div_by_multiple

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

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