fact: Record field_on (R : ring) : Type := {field_inverse_map : Map R R; field_inverse_r_prf : forall x : R, ~ Equal x (monoid_unit R) -> Equal (ring_mult x (Ap field_inverse_map x)) (ring_unit R); field_inverse_l_prf : forall x : R, ~ Equal x (monoid_unit R) -> Equal (ring_mult (Ap field_inverse_map x) x) (ring_unit R); field_unit_non_zero : ~ Equal (ring_unit R) (monoid_unit R):Prop}.
imports: Ring_cat