proposition: Lemma INTEGRAL_DOMAIN_prop : forall x y : R, Equal (ring_mult x y) (monoid_unit R) -> Equal x (monoid_unit R) \/ Equal y (monoid_unit R).
proof: Proof. intros x y H'; try assumption. generalize (INTEGRAL_DOMAIN_prop_rev (x:=x) (y:=y)). apply NNPP; tauto. Qed.
imports: Integral_domain_cat Ring_facts Classical_Prop