proposition: Theorem greatest_series_x_power_series_1 : greatest_series_x_power f 1%ser 0 = O.
proof: Proof. apply greatest_series_x_power_series_const with (c := 1%K). reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series