proposition: Theorem greatest_series_x_power_series_const : ∀ s c m, (s = series_const c)%ser → greatest_series_x_power f s m = 0%nat.
proof: Proof. intros s c m Hs. rewrite Hs. apply greatest_series_x_power_iff; simpl. remember (series_order (series_const c) (S m)) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]; [ idtac | reflexivity ]. apply series_order_iff in Hn; simpl in Hn. destruct Hn as (Hz, Hnz). exfalso; apply Hnz; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series