proposition: Theorem le_mul_0 : forall n m, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m.
proof: Proof. assert (R : forall n, 0 == n <-> n == 0) by (intros; split; apply eq_sym). intros n m. repeat rewrite lt_eq_cases. repeat rewrite R. rewrite lt_mul_0, eq_mul_0. pose proof (lt_trichotomy n 0); pose proof (lt_trichotomy m 0). tauto. Qed.
imports: ZAddOrder