proposition: Theorem greatest_series_x_power_shift : ∀ n s b, greatest_series_x_power K (series_shift n s) (b + n) = greatest_series_x_power K s b.
proof: Proof. intros n s b. remember (greatest_series_x_power K s b) as k eqn:Hk . symmetry in Hk. apply greatest_series_x_power_iff in Hk. apply greatest_series_x_power_iff. rewrite <- Nat.add_succ_l, Nat.add_comm. rewrite series_order_shift_add. remember (series_order s (S b)) as p eqn:Hp . symmetry in Hp. destruct p as [p| ]; [ idtac | assumption ]. destruct Hk as (Hz, Hnz). split. intros cnt. rewrite nth_series_order_shift. apply Hz. intros k₁ Hk₁. apply Hnz in Hk₁. destruct Hk₁ as (m, Hm). exists m; erewrite nth_series_order_shift; assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series