proposition: Theorem series_shift_add_distr : ∀ s₁ s₂ n, (series_shift n (s₁ + s₂) = series_shift n s₁ + series_shift n s₂)%ser.
proof: Proof. intros s₁ s₂ n. constructor; intros i; simpl. destruct (lt_dec i n) as [H₁| H₁]; [ idtac | reflexivity ]. rewrite rng_add_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series