proposition: Theorem series_nth_0_in_interval : ∀ s k, (∀ n, (Pos.to_nat k | nth_series_order K s 0 n)%nat) → ∀ i, (i mod Pos.to_nat k ≠ 0)%nat → (s .[i] = 0)%K.
proof: Proof. intros s k Hs i Hi. remember (rank_of_nonzero_before s i) as cnt. pose proof (Hs cnt) as H. subst cnt. unfold rank_of_nonzero_before in H. destruct i. rewrite Nat.mod_0_l in Hi; [ idtac | apply Pos2Nat_ne_0 ]. exfalso; apply Hi; reflexivity. replace (S i) with (0 + S i)%nat in H by reflexivity. apply series_nth_0_in_interval_from_any in H; auto with Arith. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series