proposition: Theorem ps_add_compat_l : ∀ ps₁ ps₂ ps₃, (ps₁ = ps₂)%ps → (ps₃ + ps₁ = ps₃ + ps₂)%ps.
proof: Proof. intros ps1 ps₂ ps₃ H₁₂. rewrite ps_add_comm; symmetry. rewrite ps_add_comm; symmetry. apply ps_add_compat_r; assumption. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add