proposition: Theorem ps_terms_add_comm : ∀ ps₁ ps₂, (ps_terms_add ps₁ ps₂ = ps_terms_add ps₂ ps₁)%ser.
proof: Proof. intros ps₁ ps₂. unfold ps_terms_add. rewrite series_add_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series