proposition: Lemma Qle_reg_mult_r_strong: forall x y z : Q, Zero <= x -> y <= z -> y * x <= z * x.
proof: Proof. intros x y z Hx Hyz; apply Qle_Zero_Qminus; stepr (x*(z-y)); [|ring]; apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; assumption. Qed.