proposition: Theorem lt_m1_mul_r : forall n m, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
proof: Proof. intros n m H; destruct (lt_trichotomy m 0) as [H1 | [H1 | H1]]. - right; right. now apply lt_1_mul_neg. - right; left; now rewrite H1, mul_0_r. - left. now apply lt_mul_m1_pos. Qed.
imports: ZAddOrder