fact: Fixpoint rank_of_nonzero_after_from s n i b := match n with | O => O | S n₁ => if lt_dec b i then match series_order s (S b) with | fin m => S (rank_of_nonzero_after_from s n₁ i (S b + m)%nat) | ∞ => O end else O end.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series