Yet another change to inverses

Apartness and having an inverse are related. It seems like they both
land in `Prop`.
More work on inverses and the field structure.