proposition: Theorem find_coeff_iter_succ : ∀ f L c pow m i 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 → (∀ n, r ≤ nth_r n f L) → (i < n)%nat → (find_coeff n pow m f L i = find_coeff (S n) pow m f L i)%K.
proof: Proof. intros f L c pow m i n r HL Hm Hq₀ Hc Hr₀ Hrle Hin. destruct (fld_zerop 1%K) as [H₀| H₀]. etransitivity; [ apply eq_1_0_all_0; assumption | ]. symmetry; apply eq_1_0_all_0; assumption. revert f L c pow m n HL Hm Hq₀ Hc Hr₀ Hrle Hin. induction i; intros. destruct n; [ exfalso; revert Hin; apply Nat.lt_irrefl | idtac ]. remember (S n) as sn. rewrite Heqsn in |- * at 1; simpl. destruct (ps_zerop _ (ps_poly_nth 0 f)) as [| H₁]; [ reflexivity | ]. remember (Nat.compare pow 0) as cmp₁ eqn:Hcmp₁ . symmetry in Hcmp₁. destruct cmp₁; [ reflexivity | | reflexivity ]. apply nat_compare_lt in Hcmp₁. exfalso; revert Hcmp₁; apply Nat.nlt_0_r. assert (0 < r)%nat as Hrp. destruct r; [ idtac | apply Nat.lt_0_succ ]. exfalso; revert Hr₀. apply multiplicity_neq_0; assumption. destruct n; [ exfalso; revert Hin; apply Nat.nlt_0_r | idtac ]. remember (S n) as sn. rewrite Heqsn in |- * at 1; simpl. destruct (ps_zerop _ (ps_poly_nth 0 f)) as [| H₁]; [ reflexivity | ]. remember (Nat.compare pow (S 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₁ . destruct (ps_zerop _ (ps_poly_nth 0 f₁)) as [H₂| H₂]. subst sn; simpl. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₃| H₃]. apply lt_S_n in Hin. destruct n; [ exfalso; revert Hin; apply Nat.nlt_0_r | simpl ]. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₄| H₄]. reflexivity. contradiction. contradiction. pose proof (Hrle 1%nat) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H. rename H into Hrle₁. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . remember (root_multiplicity acf c₁ (Φq f₁ L₁)) as r₁ eqn:Hr₁ . remember HL as H; clear HeqH. symmetry in Hr₁. eapply next_ns_r_non_decr in H; try eassumption . clear Hrle₁. 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. eapply newton_segments_not_nil in H; try eassumption . rename H into HL₁nz. remember HL₁ as H; clear HeqH. eapply hd_newton_segments in H; try eassumption. rename H into HL₁₁. remember Hf₁ as H; clear HeqH. erewrite <- nth_pol_succ with (n := O) in H; simpl; try eassumption; try reflexivity. rename H into Hf₁n. assert (∀ i : nat, i ≤ 1 → (ps_poly_nth 0 (nth_pol i f L) ≠ 0)%ps) as H. intros j Hj1. destruct j; [ assumption | idtac ]. destruct j; [ simpl; rewrite <- Hc, <- Hf₁; assumption | idtac ]. exfalso; apply le_S_n in Hj1; revert Hj1; apply Nat.nle_succ_0. rename H into Hrle₁. remember Hf₁n as H; clear HeqH. eapply first_n_pol_in_K_1_m_any_r in H; try eassumption . rename H into HK₁. remember Hini₁ as H; clear HeqH. eapply p_is_pos with (m := m) in H; try eassumption. rename H into Hppos. remember Hppos as H; clear HeqH. apply Z.lt_le_incl in H. rename H into Hpnneg. remember (next_pow pow L₁ m) as pow₁ eqn:Hpow₁ . symmetry in Hpow₁. destruct pow₁. replace pow with (0 + pow)%nat in Hpow₁ by reflexivity. rewrite next_pow_add in Hpow₁. apply Nat.eq_add_0 in Hpow₁. destruct Hpow₁ as (Hpow₁, Hpow). erewrite next_pow_eq_p with (f := f₁) in Hpow₁; try eassumption . rewrite <- Z2Nat.inj_0 in Hpow₁. apply Z2Nat.inj in Hpow₁; try assumption; [ idtac | reflexivity ]. rewrite Hpow₁ in Hppos. exfalso; revert Hppos; apply Z.lt_irrefl. remember (S pow₁) as x. rewrite <- Nat.add_1_r; subst x. rewrite <- Nat.add_1_r. do 2 rewrite find_coeff_add. subst sn. apply lt_S_n in Hin. eapply IHi; try eassumption. eapply q_eq_1_r_non_decr with (L := L); eassumption. eapply all_r_le_next with (f := f); try eassumption . 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