proposition: Theorem mul_le_mono_nonpos_r : forall n m p, p <= 0 -> n <= m -> m * p <= n * p.
proof: Proof. intros n m p H1 H2; rewrite (mul_comm n p), (mul_comm m p); now apply mul_le_mono_nonpos_l. Qed.
imports: NZAxioms NZAddOrder