fact: Record semi_field_theory : Prop := mk_sfield { SF_SR : semi_ring_theory rO rI radd rmul req; SF_1_neq_0 : ~ 1 == 0; SFdiv_def : forall p q, p / q == p * / q; SFinv_l : forall p, ~ p == 0 -> / p * p == 1 }.
imports: ZArith_base