proposition: Theorem find_coeff_more_iter : ∀ f L c pow m i n n' r, newton_segments f = Some L → pol_in_K_1_m f m → q_of_m m (γ L) = 1%positive → c = ac_root (Φq f L) → root_multiplicity acf c (Φq f L) = r → (∀ j, r ≤ nth_r j f L) → (i < n)%nat → n ≤ n' → (find_coeff n pow m f L i = find_coeff n' pow m f L i)%K.
proof: Proof. intros f L c pow m i n n' r HL Hm Hq₀ Hc Hr₀ Hrle Hin Hn'. destruct (fld_zerop 1%K) as [H₀| H₀]. etransitivity; [ apply eq_1_0_all_0; assumption | ]. symmetry; apply eq_1_0_all_0; assumption. remember (n' - n)%nat as d eqn:Hd . apply Nat.add_cancel_r with (p := n) in Hd. rewrite Nat.sub_add in Hd; [ | assumption ]. subst n'; clear Hn'. revert n pow Hin. revert f L HL Hm Hq₀ Hr₀ Hc Hrle. revert c. induction d; intros; [ reflexivity | idtac ]. erewrite find_coeff_iter_succ; try eassumption; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)) as [| H₁]; [ reflexivity | ]. remember (Nat.compare pow i) as cmp eqn:Hcmp . symmetry in Hcmp. destruct cmp; [ reflexivity | | reflexivity ]. rewrite <- Hc. remember (next_pol f (β L) (γ L) c) as f₁ eqn:Hf₁ . remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁ . remember (next_pow pow L₁ m) as pow₁. destruct (ps_zerop _ (ps_poly_nth 0 f₁)) as [H₂| H₂]. rewrite Nat.add_comm. destruct n; simpl. exfalso; revert Hin; apply Nat.nlt_0_r. destruct (ps_zerop _ (ps_poly_nth 0 f₁)) as [H₃| H₃]. reflexivity. contradiction. remember HL as H; clear HeqH. eapply next_has_ns in H; try eassumption . rename H into HL₁nz. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . remember (root_multiplicity acf c₁ (Φq f₁ L₁)) as r₁ eqn:Hr₁ . symmetry in Hr₁. pose proof (Hrle 1%nat) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁, <- Hc₁ in H. rewrite Hr₁ in H. rename H into Hrr. remember HL as H; clear HeqH. eapply next_ns_r_non_decr in H; try eassumption ; clear Hrr. destruct H as (Heq, H); move Heq at top; subst r₁. destruct H as (αj₁, (αk₁, H)). destruct H as (Hini₁, (Hfin₁, (Hαj₁, Hαk₁))). remember HL₁ as H; clear HeqH. destruct (zerop r) as [Hr| Hr]. now rewrite Hr in Hr₀; apply multiplicity_neq_0 in Hr₀. eapply hd_newton_segments in H; try eassumption. rename H into HL₁i. remember HL as H; clear HeqH. eapply first_n_pol_in_K_1_m_any_r with (n := 1%nat) in H; try eassumption; try reflexivity. simpl in H; rewrite <- Hc, <- Hf₁ in H. rename H into HK₁. apply IHd with (c := c₁); try assumption. symmetry in Hr₁. eapply q_eq_1_any_r with (f := f₁); try eassumption; reflexivity. intros j. pose proof (Hrle (S j)) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H; assumption. intros j Hj. destruct j; [ assumption | ]. apply le_S_n in Hj. apply Nat.le_0_r in Hj; rewrite Hj; simpl. rewrite <- Hc, <- Hf₁; assumption. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail