proposition: Theorem f₁_eq_term_with_Ψ_plus_sum : ∀ f L c₁ pl tl j αj l₁ l₂ r Ψ, newton_segments f = Some L → ac_root (Φq f L) = c₁ → r = root_multiplicity acf c₁ (Φq f L) → Ψ = quotient_phi_x_sub_c_pow_r (Φq f L) c₁ r → pl = [ini_pt L … oth_pts L ++ [fin_pt L]] → tl = List.map (term_of_point f) pl → l₁ = List.map (λ t, power t) tl → split_list (List.seq 0 (length (al f))) l₁ l₂ → ini_pt L = (Qnat j, αj) → (next_pol f (β L) (γ L) c₁ = POL [0%ps; 1%ps … []] ^ r * POL [ps_monom c₁ 0; 1%ps … []] ^ j * poly_inject_K_in_Kx Ψ ∘ POL [ps_monom c₁ 0; 1%ps … []] + POL [ps_monom 1%K (- β L)] * (ps_pol_summ ps_field l₁ (λ h, let āh := ps_poly_nth h f in let ah := ps_monom (coeff_of_term h tl) 0 in let αh := ord_of_pt h pl in POL [((āh - ah * ps_monom 1%K αh) * ps_monom 1%K (Qnat h * γ L))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h) + ps_pol_summ ps_field l₂ (λ l, let āl := ps_poly_nth l f in POL [(āl * ps_monom 1%K (Qnat l * γ L))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ l)))%pspol.
proof: Proof. intros f L c₁ pl tl j αj l₁ l₂ r Ψ HL Hc₁ Hr HΨ Hpl Htl Hl Hss Hini. rewrite f₁_eq_sum_without_x_β₁_plus_sum; try eassumption. rewrite sum_ah_c₁y_h_eq; try eassumption. rewrite phi_c₁y₁_psi; try eassumption. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol