proposition: Theorem f₁_eq_term_with_Ψ_plus_g : ∀ f L j αj c₁ r f₁ Ψ, newton_segments f = Some L → ini_pt L = (Qnat j, αj) → c₁ = ac_root (Φq f L) → r = root_multiplicity acf c₁ (Φq f L) → Ψ = quotient_phi_x_sub_c_pow_r (Φq f L) c₁ r → f₁ = next_pol f (β L) (γ L) c₁ → (f₁ = POL [0%ps; 1%ps … []] ^ r * POL [ps_monom c₁ 0; 1%ps … []] ^ j * POL (lap_inject_K_in_Kx (al Ψ)) ∘ POL [ps_monom c₁ 0; 1%ps … []] + g_of_ns f L)%pspol.
proof: Proof. intros f L j αj c₁ r f₁ Ψ HL Hini Hc₁ Hr HΨ Hf₁. subst f₁. remember (g_lap_of_ns f L) as gg. remember Heqgg as H; clear HeqH. unfold g_lap_of_ns in H; subst gg. rewrite <- Hc₁ in H. remember [ini_pt L … oth_pts L ++ [fin_pt L]] as pl eqn:Hpl . remember (List.map (term_of_point f) pl) as tl eqn:Htl . remember (List.map (λ t : term α nat, power t) tl) as l₁ eqn:Hl₁ . remember (list_seq_except 0 (length (al f)) l₁) as l₂ eqn:Hl₂ . symmetry in Hc₁. rewrite f₁_eq_term_with_Ψ_plus_sum with (l₂ := l₂); try eassumption. rewrite ps_poly_lap_summ; [ idtac | intros i; simpl; apply lap_eq_refl ]. rewrite ps_poly_lap_summ; [ simpl | intros i; simpl; apply lap_eq_refl ]. unfold ps_pol_add, poly_add; simpl. unfold ps_lap_add in H; simpl in H. unfold ps_lap_mul in H; simpl in H. progress unfold ps_lap_pow in H. simpl in H; rewrite <- H; clear H. reflexivity. apply except_split_seq; [ idtac | idtac | assumption ]. rewrite Hl₁, Htl, Hpl. do 2 apply Sorted_map; simpl. apply Sorted_fst_lt_nat_num_fst. intros a Ha. remember (points_of_ps_polynom f) as pts. symmetry in Heqpts. eapply pt_absc_is_nat; [ eassumption | idtac ]. eapply ns_in_init_pts; [ idtac | eassumption ]. rewrite <- Heqpts; assumption. eapply ini_oth_fin_pts_sorted; eassumption. simpl. rewrite Hl₁. apply List.Forall_forall; intros i Hi. split; [ apply Nat.le_0_l | idtac ]. apply List.in_map_iff in Hi. destruct Hi as (x, (Hxi, Hx)). subst i. rewrite Htl in Hx. apply List.in_map_iff in Hx. destruct Hx as (y, (Hi, Hy)). subst x; simpl. rename y into pt. rewrite Hpl in Hy. eapply ns_in_init_pts in Hy; [ idtac | eassumption ]. unfold points_of_ps_polynom in Hy. apply in_points_of_ps_lap_lt; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m