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