fact: Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth (sf:semi_field_theory rO rI radd rmul rdiv rinv req) := mk_afield _ _ (SRth_ARth Rsth (SF_SR sf)) (SF_1_neq_0 sf) (SFdiv_def sf) (SFinv_l sf).
imports: ZArith_base