Function vstd::arithmetic::div_mod::lemma_mod_subtraction

source · 
pub broadcast proof fn lemma_mod_subtraction(x: nat, s: nat, d: nat)
Expand description
requires
0 < d,
0 <= s <= x % d,
ensures
x % d - s % d == (x - s) % d as int,

Proof that modulo distributes over subtraction if the subtracted value is less than or equal to the modulo of the number it’s being subtracted from. Specifically, because 0 <= s <= x % d, we can conclude that x % d - s % d == (x - s) % d.