proposition: Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
proof: Proof. intros n m; split; intro H. - intro H1; apply eq_mul_0 in H1. tauto. - split; intro H1; rewrite H1 in H; (rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H. Qed.
imports: NZAxioms NZAddOrder