proposition: Theorem ps_normal_add_compat_r : ∀ ps₁ ps₂ ps₃, normalise_ps ps₁ ≐ normalise_ps ps₂ → normalise_ps (ps₁ + ps₃)%ps ≐ normalise_ps (ps₂ + ps₃)%ps.
proof: Proof. intros ps₁ ps₂ ps₃ Heq. remember (series_order (ps_terms ps₁) 0) as m₁ eqn:Hm₁ . remember (series_order (ps_terms ps₂) 0) as m₂ eqn:Hm₂ . symmetry in Hm₁, Hm₂. destruct m₁ as [m₁| ]. destruct m₂ as [m₂| ]. remember (normalise_ps ps₁) as nps₁ eqn:Hps₁ . remember (normalise_ps ps₂) as nps₂ eqn:Hps₂ . symmetry in Hps₁, Hps₂. apply normalised_exists_adjust in Hps₁. apply normalised_exists_adjust in Hps₂. destruct Hps₁ as (n₁, (k₁, Hps₁)). destruct Hps₂ as (n₂, (k₂, Hps₂)). apply eq_strong_ps_add_compat_r with (ps₃ := ps₃) in Hps₁. apply eq_strong_ps_add_compat_r with (ps₃ := ps₃) in Hps₂. rewrite Hps₁, Hps₂. rewrite <- normalise_ps_add_adjust_l. rewrite <- normalise_ps_add_adjust_l. apply eq_strong_ps_add_compat_r with (ps₃ := ps₃) in Heq. rewrite Heq; reflexivity. rewrite Hm₂; intros H; discriminate H. rewrite Hm₁; intros H; discriminate H. symmetry in Heq. eapply series_order_inf_compat in Hm₂; [ idtac | eassumption ]. rewrite Hm₁ in Hm₂; discriminate Hm₂. destruct m₂ as [m₂| ]. eapply series_order_inf_compat in Hm₁; [ idtac | eassumption ]. rewrite Hm₁ in Hm₂; discriminate Hm₂. apply eq_strong_ps_adjust_zero_neg_zero in Hm₁. apply eq_strong_ps_adjust_zero_neg_zero in Hm₂. destruct Hm₁ as (n₁, (n₂, (k₁, (k₂, Hps₁)))). destruct Hm₂ as (n₃, (n₄, (k₃, (k₄, Hps₂)))). apply eq_strong_ps_add_compat_r with (ps₃ := ps₃) in Hps₁. apply eq_strong_ps_add_compat_r with (ps₃ := ps₃) in Hps₂. rewrite normalise_ps_add_adjust_l with (n := n₁) (k := k₁). rewrite Hps₁; symmetry. rewrite normalise_ps_add_adjust_l with (n := n₃) (k := k₃). rewrite Hps₂; symmetry. rewrite <- normalise_ps_add_adjust_l. rewrite <- normalise_ps_add_adjust_l. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add