proposition: Theorem order_bbar_r_is_0 : ∀ f L m c₁ r f₁, newton_segments f = Some L → pol_in_K_1_m f m → c₁ = ac_root (Φq f L) → r = root_multiplicity acf c₁ (Φq f L) → f₁ = next_pol f (β L) (γ L) c₁ → (order (ps_poly_nth r f₁) = 0)%Qbar.
proof: Proof. intros f L m c₁ r f₁ HL Hm Hc₁ Hr Hf₁. remember (quotient_phi_x_sub_c_pow_r (Φq f L) c₁ r) as Ψ eqn:HΨ . remember HL as Hini; clear HeqHini. apply exists_ini_pt_nat in Hini. destruct Hini as (j, (αj, Hini)). rewrite f₁_eq_term_with_Ψ_plus_g; try eassumption. unfold ps_poly_nth; simpl. remember ([0%ps; 1%ps … []] ^ r)%pslap as yr. remember ([ps_monom c₁ 0; 1%ps … []] ^ j)%pslap as ycj. remember (lap_inject_K_in_Kx (al Ψ)) as psi. remember [ps_monom c₁ 0; 1%ps … []] as yc. assert (order (ps_lap_nth r (yr * ycj * psi ∘ yc)) = 0)%Qbar as Hor. subst yr ycj psi yc. progress unfold ps_lap_mul. rewrite <- lap_mul_assoc. do 2 rewrite fold_ps_lap_mul. erewrite ps_lap_nth_x_le_pow_mul; [ idtac | reflexivity ]. rewrite Nat.sub_diag. progress unfold ps_lap_mul. progress unfold lap_mul. progress unfold ps_lap_nth; simpl. rewrite list_nth_lap_convol_mul; [ idtac | reflexivity ]. unfold summation; simpl. rewrite ps_add_0_r. rewrite order_mul. rewrite fold_ps_lap_nth. rewrite ps_lap_nth_0_cons_pow. rewrite order_pow. rewrite ps_monom_order. rewrite Qbar.mul_0_r; [ idtac | intros HH; discriminate HH ]. rewrite Qbar.add_0_l. rewrite fold_ps_lap_nth. rewrite ps_lap_nth_0_apply_0. unfold ps_lap_comp. rewrite apply_lap_compose. unfold apply_lap at 2; simpl. rewrite ps_mul_0_l, ps_add_0_l. rewrite ps_mul_0_r, ps_add_0_l. rewrite apply_lap_inject_K_in_Kx_monom. rewrite ps_monom_order; [ reflexivity | idtac ]. eapply psi_c₁_ne_0 in HΨ; eassumption. eapply char_pol_root_ne_0; eassumption. intros HH. apply ps_monom_0_coeff_0 in HH. revert HH. eapply char_pol_root_ne_0; eassumption. subst yr ycj psi yc. rewrite fold_ps_lap_add. rewrite ps_lap_nth_add. rewrite fold_ps_lap_comp. rewrite order_add_eq_min; rewrite Hor. rewrite Qbar.min_l; [ reflexivity | idtac ]. apply Qbar.lt_le_incl. apply nth_g_order_pos; assumption. apply Qbar.lt_neq. apply nth_g_order_pos; 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