proposition: Theorem series_order_left_adjust : ∀ n ps, series_order (ps_terms ps) 0 = fin n → series_order (ps_terms (ps_left_adjust ps)) 0 = 0%Nbar.
proof: Proof. intros n ps Hn. unfold ps_left_adjust; simpl. rewrite Hn; simpl. apply series_order_iff. apply series_order_iff in Hn. simpl in Hn |- *. destruct Hn as (Hz, Hnz). split. intros i Hi. exfalso; revert Hi; apply Nat.nlt_0_r. rewrite Nat.add_0_r; assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series