Function vstd::arithmetic::div_mod::lemma_mod_neg_neg

source · 
pub proof fn lemma_mod_neg_neg(x: int, d: int)
Expand description
requires
0 < d,
ensures
x % d == (x * (1 - d)) % d,

Proof that the remainder when dividing integer x by positive integer d is equivalent to the remainder of x * (1 - d) by d.