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