proposition: Theorem lap_f₁_eq_x_min_β₁_comp : ∀ la β₁ γ₁ c₁, (next_lap la β₁ γ₁ c₁ = [ps_monom 1%K (- β₁)] * la ∘ ([ps_monom 1%K γ₁] * [ps_monom c₁ 0; 1%ps … []]))%pslap.
proof: Proof. intros la β₁ γ₁ c₁. progress unfold next_lap. apply lap_mul_compat; [ reflexivity | idtac ]. apply lap_compose_compat; [ reflexivity | idtac ]. progress unfold ps_lap_mul, lap_mul; simpl. progress unfold summation; simpl. rewrite rng_mul_0_l. do 3 rewrite rng_add_0_r. simpl. constructor. rewrite ps_mul_comm; simpl. apply ps_monom_split_mul. constructor; [ idtac | reflexivity ]. rewrite rng_mul_1_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