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.