proposition: Theorem series_order_shift : ∀ s n, series_order (series_shift n s) 0 = (fin n + series_order s 0)%Nbar.
proof: Proof. intros s n. induction n. rewrite series_shift_0, Nbar.add_0_l; reflexivity. rewrite series_order_shift_S; [ idtac | apply Nat.le_0_l ]. rewrite IHn; simpl. destruct (series_order s); reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series