fact: Definition ps_inv {α} {r : ring α} {f : field r} ps := match series_order (ps_terms ps) O with | fin n => {| ps_terms := series_inv (series_left_shift n (ps_terms ps)); ps_ordnum := - ps_ordnum ps - Z.of_nat n; ps_polydo := ps_polydo ps |} | ∞ => ps end.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series