proposition: Theorem ps_normal_mul_compat_r : ∀ ps₁ ps₂ ps₃, normalise_ps ps₁ ≐ normalise_ps ps₂ → normalise_ps (ps_mul ps₁ ps₃) ≐ normalise_ps (ps_mul ps₂ ps₃).
proof: Proof. intros ps₁ ps₂ ps₃ Heq. remember Heq as Heqv; clear HeqHeqv. remember (normalise_ps ps₁) as nps₁ eqn:Hps₁ in Heq. remember (normalise_ps ps₂) as nps₂ eqn:Hps₂ in Heq. symmetry in Hps₁, Hps₂. 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₁| ]. apply normalised_exists_adjust in Hps₁. destruct m₂ as [m₂| ]. apply normalised_exists_adjust in Hps₂. destruct Hps₁ as (n₁, (k₁, Hps₁)). destruct Hps₂ as (n₂, (k₂, Hps₂)). apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Hps₁. apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Hps₂. rewrite Hps₁, Hps₂. rewrite <- normalise_ps_mul_adjust_l. rewrite <- normalise_ps_mul_adjust_l. apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Heq. rewrite Heq; reflexivity. intros H; rewrite Hm₂ in H; discriminate H. symmetry in Heqv. eapply series_order_inf_compat in Hm₂; [ idtac | eassumption ]. rewrite Hm₁ in Hm₂; discriminate Hm₂. intros H; rewrite Hm₁ in H; discriminate H. clear Hm₂. remember Hm₁ as Hm₂; clear HeqHm₂. eapply series_order_inf_compat in Hm₂; [ idtac | eassumption ]. 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₂, Hm₁)))). destruct Hm₂ as (n₃, (n₄, (k₃, (k₄, Hm₂)))). apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Hm₁. apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Hm₂. rewrite normalise_ps_mul_adjust_l with (n := n₁) (k := k₁). rewrite Hm₁; symmetry. rewrite normalise_ps_mul_adjust_l with (n := n₃) (k := k₃). rewrite Hm₂; symmetry. rewrite <- normalise_ps_mul_adjust_l. rewrite <- normalise_ps_mul_adjust_l. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat