proposition: Theorem series_nth_mul_stretch : ∀ s k i, (series_stretch k s) .[Pos.to_nat k * i] = s .[i].
proof: Proof. intros s k i; simpl. rewrite Nat.mul_comm. rewrite Nat.mod_mul; [ simpl | apply Pos2Nat_ne_0 ]. rewrite Nat.div_mul; [ simpl | apply Pos2Nat_ne_0 ]. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series