proposition: Theorem greatest_series_x_power_stretch_inf : ∀ s b k, series_order s (S b) = ∞ → greatest_series_x_power K (series_stretch k s) (b * Pos.to_nat k) = O.
proof: Proof. intros s b k Hs. remember (greatest_series_x_power K s b) as n eqn:Hn . symmetry in Hn. apply greatest_series_x_power_iff in Hn. apply greatest_series_x_power_iff. rewrite Hs in Hn. rewrite series_order_stretch_succ_inf; auto. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series