proposition: Theorem f₁_eq_x_min_β₁_summation : ∀ f β₁ γ₁ c₁, (next_pol f β₁ γ₁ c₁ = POL [ps_monom 1%K (- β₁)] * ps_pol_summ ps_field (List.seq 0 (length (al f))) (λ h, let āh := ps_poly_nth h f in POL [(āh * ps_monom 1%K (Qnat h * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h))%pspol.
proof: Proof. intros f β₁ γ₁ c. rewrite f₁_eq_x_min_β₁_comp. progress unfold ps_pol_comp. rewrite poly_compose_compose2. apply poly_mul_compat; [ reflexivity | idtac ]. progress unfold poly_compose2; simpl. progress unfold lap_compose2, poly_summation; simpl. progress unfold eq_poly; simpl. apply list_fold_right_compat; [ idtac | reflexivity ]. intros la lb i Heq. apply lap_add_compat; [ assumption | idtac ]. progress unfold ps_poly_nth, ps_lap_nth. rewrite lap_power_mul. rewrite lap_mul_assoc. apply lap_mul_compat; [ idtac | reflexivity ]. clear la lb Heq. remember (al f) as la; clear f Heqla. revert la. induction i; intros; simpl. rewrite lap_mul_1_r. constructor; [ idtac | reflexivity ]. progress unfold Qnat; simpl. rewrite <- ps_mul_1_r in |- * at 1. apply ps_mul_compat_l. rewrite Qmult_0_l; reflexivity. destruct la as [| a]; simpl. rewrite lap_mul_assoc; simpl. rewrite lap_eq_0. rewrite lap_mul_nil_l. rewrite lap_mul_nil_l. constructor; [ idtac | reflexivity ]. simpl. rewrite ps_mul_0_l; reflexivity. rewrite lap_mul_assoc. rewrite lap_mul_shuffle0. rewrite IHi. progress unfold lap_mul; simpl. rewrite summation_only_one; simpl. constructor; [ idtac | reflexivity ]. simpl. rewrite <- ps_mul_assoc. apply ps_mul_compat_l. rewrite ps_monom_mul_r_pow; symmetry. rewrite ps_monom_mul_r_pow; symmetry. rewrite rng_mul_shuffle0; simpl. rewrite rng_mul_assoc; simpl. 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