fact: Fixpoint nth_series_order α (R : ring α) (K : field R) s b n := match series_order s (S b) with | fin p => match n with | O => S p | S n₁ => nth_series_order K s (S b + p)%nat n₁ end | ∞ => O end.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series