proposition: Theorem ncrl_inf_gsxp : ∀ s n, series_order s (S n) = ∞ → greatest_series_x_power K s n = O.
proof: Proof. intros s n Hn. apply greatest_series_x_power_iff. rewrite Hn; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series