proposition: Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n.
proof: Proof. intros n m p H1 H2. le_elim H1. - le_elim H2. + apply lt_le_incl. now apply mul_lt_mono_neg_l. + apply eq_le_incl; now rewrite H2. - apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l. Qed.
imports: NZAxioms NZAddOrder