proposition: Theorem series_series_order_inf_iff : ∀ s, series_order s 0 = ∞ ↔ (s = 0)%ser.
proof: Proof. intros s. split; intros H. apply series_order_iff in H. simpl in H. constructor; assumption. apply series_order_iff; simpl. inversion_clear H; assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series