proposition: Theorem greatest_series_x_power_left_shift : ∀ s n p, greatest_series_x_power K (series_left_shift n s) p = greatest_series_x_power K s (n + p).
proof: Proof. intros s n p. remember (greatest_series_x_power K s (n + p)) as k eqn:Hk . symmetry in Hk. apply greatest_series_x_power_iff in Hk. apply greatest_series_x_power_iff. pose proof (nth_series_order_left_shift s n O p) as H. simpl in H. remember (series_order s (S (n + p))) as n₁ eqn:Hn₁ . remember (series_order (series_left_shift n s) (S p)) as n₂ eqn:Hn₂ . symmetry in Hn₁, Hn₂. destruct n₁ as [n₁| ]. destruct n₂ as [n₂| ]; [ idtac | discriminate H ]. destruct Hk as (Hxp, Hnxp). split. unfold is_a_series_in_x_power in Hxp |- *. rename n into m. intros n. rewrite nth_series_order_left_shift. apply Hxp. intros k₁ Hk₁. apply Hnxp in Hk₁. destruct Hk₁ as (m, Hm). exists m. rewrite nth_series_order_left_shift. assumption. destruct n₂; [ discriminate H | assumption ]. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series