proposition: Theorem series_null_power : ∀ s b p, is_a_series_in_x_power s b p → ∀ i, ((i - b) omod p)%nat ≠ O → (s .[i] = 0)%K.
proof: Proof. intros s b p Hxp i Hip. destruct p; [ exfalso; apply Hip; reflexivity | idtac ]. destruct (le_dec i b) as [H₁| H₁]. apply Nat.sub_0_le in H₁. rewrite H₁, omod_0_l in Hip; auto with Arith. exfalso; apply Hip; reflexivity. apply Nat.nle_gt in H₁. remember (i - b)%nat as j eqn:Hj . symmetry in Hj. apply Nat.add_sub_eq_nz in Hj. subst i. remember (Pos.of_nat (S p)) as q eqn:Hq . apply series_nth_0_in_interval_from_any with (c := S j) (k := q). apply Nat.lt_succ_r; reflexivity. subst q; rewrite Nat2Pos.id; auto with Arith. unfold is_a_series_in_x_power in Hxp. subst q; rewrite Nat2Pos.id; auto with Arith. subst q; rewrite Nat2Pos.id; auto with Arith. intros H; apply Hip; rewrite H; clear H. apply Nat.mod_0_l; intros H; discriminate H. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series