proposition: Lemma FIELD_law_inverse : forall x y : K, Equal (ring_mult x y) (ring_unit K) -> Equal (field_inverse x) y.
proof: Proof. intros x y H'; try assumption. apply FIELD_reg_left with x. apply FIELD_integral_domain_l with y; auto with algebra. intuition. absurd (Equal (ring_unit K) (monoid_unit K)); auto with algebra. apply Trans with (ring_mult x y:K); auto with algebra. apply Trans with (ring_unit K:K); auto with algebra. apply FIELD_inverse_r. intuition. absurd (Equal (ring_unit K) (monoid_unit K)); auto with algebra. apply Trans with (ring_mult x y:K); auto with algebra. apply Trans with (ring_mult (monoid_unit K) y:K); auto with algebra. Qed.
imports: Field_cat Ring_facts