proposition: Theorem lt_0_mul n m : 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
proof: Proof. split; [intro H | intros [[H1 H2] | [H1 H2]]]. - destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; [| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |]; (destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; [| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]); try (left; now split); try (right; now split). + assert (H3 : n * m < 0) by now apply mul_neg_pos. exfalso; now apply (lt_asymm (n * m) 0). + assert (H3 : n * m < 0) by now apply mul_pos_neg. exfalso; now apply (lt_asymm (n * m) 0). - now apply mul_pos_pos. - now apply mul_neg_neg. Qed.
imports: NZAxioms NZAddOrder