fact: Definition adjust_ps α {R : ring α} n k ps := {| ps_terms := series_shift n (series_stretch k (ps_terms ps)); ps_ordnum := ps_ordnum ps * Zpos k - Z.of_nat n; ps_polydo := ps_polydo ps * k |}.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series