proposition: Theorem ps_mul_compat_l : ∀ ps₁ ps₂ ps₃, (ps₁ = ps₂)%ps → (ps₃ * ps₁ = ps₃ * ps₂)%ps.
proof: Proof. intros ps₁ ps₂ ps₃ Heq. rewrite ps_mul_comm; symmetry. rewrite ps_mul_comm; symmetry. apply ps_mul_compat_r; assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat