proposition: Theorem series_stretch_add_distr : ∀ k s₁ s₂, (series_stretch k (s₁ + s₂) = series_stretch k s₁ + series_stretch k s₂)%ser.
proof: Proof. intros kp s₁ s₂. constructor; intros i; simpl. remember (Pos.to_nat kp) as k. assert (k ≠ O) as Hk by (subst k; apply Pos2Nat_ne_0). destruct (zerop (i mod k)); [ reflexivity | idtac ]. rewrite rng_add_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series