proposition: Theorem series_order_inf_compat : ∀ ps₁ ps₂, normalise_ps ps₁ ≐ normalise_ps ps₂ → series_order (ps_terms ps₁) 0 = ∞ → series_order (ps_terms ps₂) 0 = ∞.
proof: Proof. intros ps₁ ps₂ Heq Hinf. apply ps_series_order_inf_iff in Hinf. apply ps_series_order_inf_iff. inversion Hinf; constructor. rewrite <- Heq, H; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add