proposition: Theorem series_order_inf_left_adjust : ∀ ps, series_order (ps_terms ps) 0 = ∞ → series_order (ps_terms (ps_left_adjust ps)) 0 = ∞.
proof: Proof. intros ps Hn. apply series_order_iff. unfold ps_left_adjust; simpl. rewrite Hn. apply series_order_iff in Hn. assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series