proposition: Theorem series_stretch_series_0 : ∀ k, (series_stretch k 0 = 0)%ser.
proof: Proof. intros k. constructor; intros i; simpl. destruct (zerop (i mod Pos.to_nat k)); [ idtac | reflexivity ]. destruct (Nbar.lt_dec (fin (i / Pos.to_nat k)) 0); reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series