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