proposition: Theorem eq_mul_0 : forall n m, n * m == 0 <-> n == 0 \/ m == 0.
proof: Proof. intros n m; split. - intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; try (now right); try (now left). + exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |]. + exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |]. + exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |]. + exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |]. - intros [H | H]. + now rewrite H, mul_0_l. + now rewrite H, mul_0_r. Qed.
imports: NZAxioms NZAddOrder