fact: Definition adjust_ps_from α {R : ring α} (ps₁ ps₂ : puiseux_series α) := let k₁ := ps_polydo ps₂ in let k₂ := ps_polydo ps₁ in let v₁ := (ps_ordnum ps₁ * Zpos k₁)%Z in let v₂ := (ps_ordnum ps₂ * Zpos k₂)%Z in adjust_ps (Z.to_nat (v₂ - Z.min v₁ v₂)) k₂ ps₂.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series