proposition: Theorem series_nth_0_series_nth_shift_0 : ∀ s n, (∀ i, (s .[i] = 0)%K) → ∀ i, ((series_shift n s) .[i] = 0)%K.
proof: Proof. intros s n H i; simpl. destruct (lt_dec i n) as [| H₁]; [ reflexivity | idtac ]. apply H. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add