proposition: Theorem series_left_shift_left_shift : ∀ (s : power_series α) m n, (series_left_shift m (series_left_shift n s) = series_left_shift (m + n) s)%ser.
proof: Proof. intros s m n. constructor; intros i; simpl. rewrite Nat.add_comm, Nat.add_shuffle0; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series