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