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