proposition: Theorem eq_ps_add_add₂ : ∀ ps₁ ps₂, (ps₁ + ps₂ = ps_add₂ ps₁ ps₂)%ps.
proof: Proof. intros ps₁ ps₂. constructor. apply eq_strong_ps_normal_add_add₂. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series