proposition: Lemma Qmult_Qlt_Qle_nonneg_pos_compat: forall n m p q, n < p -> m <= q -> Zero <= n -> Zero < q -> n * m < p * q.
proof: Proof. intros n m p q H1 H2 H3 H4; apply Qle_lt_trans with (n*q); [ apply Qle_reg_mult_l_strong|apply Qlt_reg_mult_pos_r; trivial; apply Qlt_le_trans with m]; trivial. Qed.