proposition: Theorem nth_series_order_left_shift : ∀ s m n p, nth_series_order K (series_left_shift m s) p n = nth_series_order K s (m + p) n.
proof: Proof. intros s m n p. revert m p. induction n; intros; simpl. rewrite series_order_succ2; symmetry. rewrite series_order_succ2; symmetry. rewrite series_left_shift_left_shift. rewrite Nat.add_comm; reflexivity. rewrite series_order_succ2; symmetry. rewrite series_order_succ2; symmetry. rewrite series_left_shift_left_shift. rewrite Nat.add_comm. remember (series_order (series_left_shift (m + p) s) 1) as q. symmetry in Heqq. destruct q as [q| ]. symmetry. rewrite <- Nat.add_assoc, <- Nat.add_succ_r. symmetry. apply IHn. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series