proposition: Theorem lt_mul_m1_pos : forall n m, n < -1 -> 0 < m -> n * m < -1.
proof: Proof. intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1. - rewrite mul_opp_l, mul_1_l in H1. apply opp_neg_pos in H2. now apply lt_m1_r with (- m). - assumption. Qed.
imports: ZAddOrder