proposition: Theorem eq_strong_ps_add_comm : ∀ ps₁ ps₂, (ps₁ + ps₂)%ps ≐ (ps₂ + ps₁)%ps.
proof: Proof. intros ps₁ ps₂. constructor; simpl. apply Z.min_comm. apply Pos.mul_comm. apply ps_terms_add_comm. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series