proposition: Lemma FIELD_inverse_inverse : forall x : K, ~ Equal x (monoid_unit K) -> Equal (field_inverse (field_inverse x)) x.
proof: Proof. intros x H'; try assumption. apply FIELD_reg_right with (field_inverse x); auto with algebra. apply Trans with (ring_unit K:K); auto with algebra. apply Sym; auto with algebra. Qed.
imports: Field_cat Ring_facts