fact: Definition ps_ordnum_add α (ps₁ ps₂ : puiseux_series α) := let k₁ := cm_factor ps₁ ps₂ in let k₂ := cm_factor ps₂ ps₁ in let v₁ := (ps_ordnum ps₁ * Zpos k₁)%Z in let v₂ := (ps_ordnum ps₂ * Zpos k₂)%Z in Z.min v₁ v₂.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series