proposition: Theorem series_nth_0_in_interval_from_any : ∀ s i c b k, (i < c)%nat → (∀ n, (Pos.to_nat k | nth_series_order K s b n)%nat) → (Pos.to_nat k | nth_series_order K s b (pred (rank_of_nonzero_after_from s c (b + i) b)))%nat → i mod Pos.to_nat k ≠ O → (s .[b + i] = 0)%K.
proof: Proof. intros s i c b k Hic Has Hs Hm. remember (pred (rank_of_nonzero_after_from s c (b + i) b)) as n eqn:Hn . symmetry in Hn. destruct c; [ exfalso; revert Hic; apply Nat.nlt_0_r | simpl in Hn ]. destruct i. rewrite Nat.mod_0_l in Hm; [ idtac | apply Pos2Nat_ne_0 ]. exfalso; apply Hm; reflexivity. apply Nat.succ_lt_mono in Hic. destruct (lt_dec b (b + S i)) as [H₁| H₁]. clear H₁. remember (series_order s (S b)) as len eqn:Hlen . symmetry in Hlen. destruct len as [len| ]. simpl in Hn. revert i b len n Has Hic Hlen Hn Hs Hm. induction c; intros; [ exfalso; revert Hic; apply Nat.nlt_0_r | idtac ]. simpl in Hn. destruct (lt_dec (S (b + len)) (b + S i)) as [H₁| H₁]. rewrite Nat.add_succ_r in H₁. apply Nat.succ_lt_mono in H₁. apply Nat.add_lt_mono_l in H₁. remember (series_order s (S (S (b + len)))) as len₁. rename Heqlen₁ into Hlen₁. symmetry in Hlen₁. destruct len₁ as [len₁| ]. destruct n; [ discriminate Hn | idtac ]. apply Nat.succ_inj in Hn. destruct i; [ exfalso; revert H₁; apply Nat.nlt_0_r | idtac ]. apply Nat.succ_lt_mono in Hic. apply Nat.succ_le_mono in H₁. replace (b + S (S i))%nat with (S (b + len) + S (i - len))%nat . eapply IHc; try eassumption. intros m. pose proof (Has (S m)) as H; simpl in H. rewrite Hlen in H; assumption. eapply Nat.le_lt_trans; [ apply Nat.le_sub_l | auto ]. replace (S (b + len) + S (i - len))%nat with (b + S (S i))%nat . simpl; apply Hn. simpl. do 3 rewrite Nat.add_succ_r. do 2 apply Nat.succ_inj_wd. rewrite <- Nat.add_assoc. apply Nat.add_cancel_l. rewrite Nat.add_comm. rewrite Nat.sub_add; [ reflexivity | assumption ]. simpl in Hs. rewrite Hlen in Hs; assumption. replace (S (S i)) with (S (i - len) + S len)%nat in Hm . pose proof (Has O) as H; simpl in H. rewrite Hlen in H. rewrite Nat.add_mod in Hm; auto with Arith. destruct H as (c₁, Hc₁). rewrite Hc₁ in Hm. rewrite Nat.mod_mul, Nat.add_0_r in Hm; auto with Arith. rewrite Nat.mod_mod in Hm; auto with Arith. rewrite Nat.add_succ_l, Nat.add_succ_r. do 2 apply Nat.succ_inj_wd. rewrite Nat.sub_add; [ reflexivity | assumption ]. do 3 rewrite Nat.add_succ_r. rewrite Nat.add_succ_l. do 2 apply Nat.succ_inj_wd. rewrite <- Nat.add_assoc. apply Nat.add_cancel_l. rewrite Nat.add_comm. rewrite Nat.sub_add; [ reflexivity | assumption ]. apply series_order_iff in Hlen₁; simpl in Hlen₁. pose proof (Hlen₁ (i - len - 1)%nat) as H. replace (b + S i)%nat with (S (S (b + len + (i - len - 1)))) . assumption. rewrite Nat.add_succ_r. apply Nat.succ_inj_wd. rewrite <- Nat.sub_add_distr, Nat.add_1_r. rewrite <- Nat.add_succ_l, <- Nat.add_succ_r. rewrite <- Nat.add_assoc. rewrite Nat.add_sub_assoc; auto with Arith. rewrite Nat.add_sub_swap; auto with Arith. rewrite Nat.sub_diag; reflexivity. apply Nat.nlt_ge in H₁. rewrite Nat.add_succ_r in H₁. apply Nat.succ_le_mono in H₁. apply Nat.add_le_mono_l in H₁. destruct (eq_nat_dec i len) as [H₂| H₂]. subst n len. simpl in Hs. rewrite Hlen in Hs. destruct Hs as (c₁, Hc₁). rewrite Hc₁ in Hm. rewrite Nat.mod_mul in Hm; auto with Arith. exfalso; apply Hm; reflexivity. apply series_order_iff in Hlen; simpl in Hlen. destruct Hlen as (Hz, Hnz). rewrite Nat.add_succ_r. apply Hz, Nat_le_neq_lt; assumption. rewrite Nat.add_succ_r. apply series_order_iff in Hlen; simpl in Hlen. apply Hlen. exfalso; apply H₁. apply Nat.lt_sub_lt_add_l. rewrite Nat.sub_diag. apply Nat.lt_0_succ. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series