fact: Definition ps_terms_add α {R : ring α} (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 let n₁ := Z.to_nat (v₁ - Z.min v₁ v₂) in let n₂ := Z.to_nat (v₂ - Z.min v₂ v₁) in let s₁ := adjust_series n₁ k₁ (ps_terms ps₁) in let s₂ := adjust_series n₂ k₂ (ps_terms ps₂) in series_add s₁ s₂.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series