proposition: Theorem mul_lt_mono_nonpos : forall n m p q, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p.
proof: Proof. intros n m p q H1 H2 H3 H4. apply le_lt_trans with (m * p). - apply mul_le_mono_nonpos_l; [assumption | now apply lt_le_incl]. - apply -> mul_lt_mono_neg_r; [assumption | now apply lt_le_trans with q]. Qed.
imports: ZAddOrder