Function vstd::arithmetic::div_mod::lemma_div_is_ordered_by_denominator
source · pub broadcast proof fn lemma_div_is_ordered_by_denominator(x: int, y: int, z: int)Expand description
requires
0 <= x,1 <= y <= z,#[trigger] (x / y) >= #[trigger] (x / z),Proof that given two fractions with the same numerator, the order
of the fractions is determined by the denominators. However, if
the numerator is 0, the fractions are equal regardless of the
denominators’ values. Specifically, given that 1 <= y <= z, we
know x / y >= x / z.