Library Coq.setoid_ring.Integral_domain

Require Export Cring.


Class Integral_domain {R : Type}`{Rcr:Cring R} := {
 integral_domain_product:
   forall x y, x * y == 0 -> x == 0 \/ y == 0;
 integral_domain_one_zero: not (1 == 0)}.

Section integral_domain.

Context {R:Type}`{Rid:Integral_domain R}.

Lemma integral_domain_minus_one_zero: ~ - (1:R) == 0.

Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N.of_nat n).

Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0.

Lemma Rintegral_domain_pow:
  forall c p r, ~c == 0 -> c * (pow p r) == ring0 -> p == ring0.

End integral_domain.