proposition: Lemma Qmult_le_compat_nonneg: forall x y z t : Q, 0 <= x <= y -> 0 <= z <= t -> x * z <= y * t.
proof: Proof. intros [xn xd] [yn yd] [zn zd] [tn td] [H0lex Hxlty] [H0lez Hzltt]. unfold Qmult, Qlt, Qle, Qnum, Qden in *. rewrite Z.mul_0_l,Z.mul_1_r in H0lex, H0lez. do 2 rewrite Pos2Z.inj_mul. setoid_replace (xn * zn * (Z.pos yd * Z.pos td))%Z with ((xn * Z.pos yd) * (zn * Z.pos td))%Z by ring. setoid_replace (yn * tn * (Z.pos xd * Z.pos zd))%Z with ((yn * Z.pos xd) * (tn * Z.pos zd))%Z by ring. apply Z.mul_le_mono_nonneg. 2,4 : assumption. 1,2 : rewrite <- (Z.mul_0_l 0); apply Z.mul_le_mono_nonneg; [reflexivity|assumption|reflexivity|apply Pos2Z.is_nonneg]. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool