proposition: Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m.
proof: Proof. intros n m p H1 H2. le_elim H1. - le_elim H2. + apply lt_le_incl. now apply mul_lt_mono_pos_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