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.