proposition: Theorem series_left_shift_stretch : ∀ s n k, (series_left_shift (n * Pos.to_nat k) (series_stretch k s) = series_stretch k (series_left_shift n s))%ser.
proof: Proof. intros s n k. constructor; intros i; simpl. rewrite Nat.add_comm. rewrite Nat.mod_add; auto with Arith. rewrite Nat.div_add; auto with Arith. destruct (zerop (i mod Pos.to_nat k)) as [H₂| H₂]; [ idtac | reflexivity ]. rewrite Nat.add_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series