proposition: Theorem eq_strong_ps_add_compat_r : ∀ ps₁ ps₂ ps₃, eq_ps_strong ps₁ ps₂ → eq_ps_strong (ps₁ + ps₃)%ps (ps₂ + ps₃)%ps.
proof: Proof. intros ps₁ ps₂ ps₃ Heq. induction Heq. unfold ps_add. constructor; simpl. unfold ps_ordnum_add. unfold cm_factor. rewrite H, H0. reflexivity. unfold cm. rewrite H0; reflexivity. unfold ps_terms_add. unfold cm_factor. unfold adjust_series. rewrite H, H0, H1. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add