proposition: Theorem phi_c₁y₁_psi : ∀ f L pl tl l c₁ r Ψ j αj, 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 → ini_pt L = (Qnat j, αj) → (POL [ps_monom c₁ 0; 1%ps … []] ^ j * ps_pol_comp (poly_inject_K_in_Kx (Φq f L)) (POL [ps_monom c₁ 0; 1%ps … []]) = POL [0%ps; 1%ps … []] ^ r * POL [ps_monom c₁ 0; 1%ps … []] ^ j * ps_pol_comp (poly_inject_K_in_Kx Ψ) (POL [ps_monom c₁ 0; 1%ps … []]))%pspol.
proof: Proof. intros f L pl tl l c₁ r Ψ j αj HL Hc₁ Hr HΨ Hpl Htl Hl Hini. remember HL as Hfin; clear HeqHfin. apply exists_fin_pt_nat in Hfin. destruct Hfin as (k, (αk, Hk)). symmetry. progress unfold ps_pol_mul. rewrite poly_mul_comm, poly_mul_assoc, poly_mul_comm. apply poly_mul_compat; [ reflexivity | idtac ]. rewrite phi_zq_eq_z_sub_c₁_psi; try eassumption. rewrite poly_inject_inj_mul. progress unfold eq_poly; simpl. rewrite <- lap_power_map_ps; simpl. rewrite lap_compose_mul. symmetry. rewrite lap_mul_comm. apply lap_mul_compat_l. clear Hr HΨ. induction r. simpl; progress unfold summation; simpl. rewrite rng_mul_0_l, rng_add_0_l, rng_add_0_l. reflexivity. rewrite <- Nat.add_1_r. unfold ps_lap_pow. do 2 rewrite lap_power_add. do 2 rewrite lap_power_1. rewrite lap_compose_mul. rewrite IHr. apply lap_mul_compat_l; simpl. progress unfold summation; simpl. rewrite rng_mul_0_l, rng_add_0_l, rng_add_0_l. rewrite rng_add_0_r, rng_add_0_r, rng_mul_1_r. constructor; [ idtac | reflexivity ]. rewrite ps_mul_1_l, ps_monom_opp, ps_add_opp_r. 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