proposition: Lemma INTEGRAL_DOMAIN_prop_rev : forall x y : R, ~ Equal x (monoid_unit R) -> ~ Equal y (monoid_unit R) -> ~ Equal (ring_mult x y) (monoid_unit R).
proof: Proof. exact (idomain_prf R). Qed.
imports: Integral_domain_cat Ring_facts Classical_Prop