proposition: Theorem lt_mul_r : forall n m p, 0 < n -> 1 < p -> n < m -> n < m * p.
proof: Proof. intros n m p **. stepl (n * 1) by now rewrite mul_1_r. apply mul_lt_mono_nonneg. - now apply lt_le_incl. - assumption. - apply le_0_1. - assumption. Qed.
imports: ZAddOrder