Function vstd::arithmetic::div_mod::lemma_div_multiples_vanish_quotient

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

Proof that multiplying the numerator and denominator by an integer does not change the quotient. Specifically, a / d == (x * a) / (x * d).