proposition: Lemma INTEGRAL_DOMAIN_mult_r : forall x y : R, ~ Equal (ring_mult x y) (monoid_unit R) -> ~ Equal y (monoid_unit R).
proof: Proof. unfold not in |- *. intros x y H' H'0; try assumption. absurd (Equal (ring_mult x y) (monoid_unit R)); auto with algebra. apply Trans with (ring_mult x (monoid_unit R)); auto with algebra. Qed.
imports: Integral_domain_cat Ring_facts Classical_Prop