proposition: Theorem series_nth_add_left_shift : ∀ (s : power_series α) i n, s .[i + n] = (series_left_shift n s) .[i].
proof: Proof. intros s i n; simpl. rewrite Nat.add_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series