Function vstd::arithmetic::div_mod::lemma_part_bound2

source · 
pub broadcast proof fn lemma_part_bound2(x: int, y: int, z: int)
Expand description
requires
0 <= x,
0 < y,
0 < z,
ensures
y * z > 0,
#[trigger] (x % y) % #[trigger] (y * z) < y,

Proof that (x % y) % (y * z) < y.