Discrete fields

[Taneb]

We have one approach to fields in Algebra.Apartness.{Structures,Bundles}. Another, stricter, approach is what nlab calls a "discrete field". This is a commutative ring with the following properties:

invertibleOrZero : ∀ x → Invertible 1# _*_ x ⊎ x ≈ 0#
¬invertibleAndZero : ∀ x → ¬ (Invertible 1# _*_ x × x ≈ 0#)

Any discrete field is a Heyting field. We should also prove that ℚᵘ and ℚ are fields.