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