Function vstd::arithmetic::div_mod::lemma_div_denominator

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

Proof that dividing x by c * d is equivalent to first dividing x by c and then dividing the result by d