proposition: Theorem mul_le_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_trans with (m * p). - now apply mul_le_mono_nonpos_l. - apply mul_le_mono_nonpos_r; [now apply le_trans with q | assumption]. Qed.
imports: ZAddOrder