pub proof fn lemma_truncate_middle(x: int, b: int, c: int)Expand description
requires
0 <= x,0 < b,0 < c,0 < b * c,(b * x) % (b * c) == b * (x % c),Proof that common factors from the dividend and divisor of a
modulus operation can be factored out. Specifically,
(b * x) % (b * c) == b * (x % c).