Function vstd::arithmetic::div_mod::lemma_div_is_ordered

x <= y,

0 < z,

#[trigger] (x / z) <= #[trigger] (y / z),

Proof that numerical order is preserved when dividing two seperate integers by a common positive divisor. Specifically, given that z > 0 and x <= y, we know x / z <= y / z.