proposition: Theorem nth_series_order_shift : ∀ s cnt n b, nth_series_order K (series_shift n s) (b + n) cnt = nth_series_order K s b cnt.
proof: Proof. intros s cnt n b. revert b. induction cnt; intros; simpl. rewrite <- Nat.add_succ_l, Nat.add_comm. rewrite series_order_shift_add. destruct (series_order s (S b)); reflexivity. rewrite <- Nat.add_succ_l, Nat.add_comm. rewrite series_order_shift_add. remember (series_order s (S b)) as m eqn:Hm . symmetry in Hm. destruct m as [m| ]; [ idtac | reflexivity ]. rewrite Nat.add_shuffle0. rewrite <- Nat.add_succ_l. apply IHcnt. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series