proposition: Theorem series_shift_series_0 : ∀ n, (series_shift n 0 = 0)%ser.
proof: Proof. intros n. constructor; intros i; simpl. destruct (lt_dec i n); reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series