proposition: Lemma FIELD_inverse_non_zero : forall x : K, ~ Equal x (monoid_unit K) -> ~ Equal (field_inverse x) (monoid_unit K).
proof: Proof. intuition. apply FIELD_unit_non_zero. apply Trans with (ring_mult (field_inverse x) x:K); auto with algebra. apply Sym; auto with algebra. apply Trans with (ring_mult (monoid_unit K) x:K); auto with algebra. Qed.
imports: Field_cat Ring_facts