proposition: Lemma Qmult_Qle_compat: forall n m p q : Q, n <= p -> m <= q -> Zero <= n -> Zero <= m -> n * m <= p * q.
proof: Proof. intros n m p a Hnp Hmq Hn Hm; case (Qle_lt_eq_dec _ _ Hm); clear Hm; intro Hm; [case (Qle_lt_eq_dec _ _ Hn); clear Hn; intro Hn; [ apply Qle_trans with (p*m); [ apply Qle_reg_mult_r | apply Qle_reg_mult_l; trivial; apply Qlt_le_trans with n ] | subst n; stepl Zero; auto; apply Qle_mult_nonneg_nonneg; trivial; match goal with | [ id: (Qlt Zero ?X1) |- _ ] => apply Qle_trans with X1; trivial; apply Qlt_le_weak end ] |subst m; stepl Zero; try ring; apply Qle_mult_nonneg_nonneg; trivial; apply Qle_trans with n ] ;trivial. Qed.