Division_Ring.V
module I : sig ... end
val non_zero_ring : bool
val multiplicative_inverse : D.t -> bool