proposition: Lemma FIELD_unit_inverse : Equal (field_inverse (ring_unit K)) (ring_unit K).
proof: Proof. apply Trans with (ring_mult (field_inverse (ring_unit K)) (ring_unit K)); auto with algebra. Qed.
imports: Field_cat Ring_facts