proposition: Theorem minus_beta_in_K_1_mq : ∀ f L m a c q, newton_segments f = Some L → pol_in_K_1_m f m → q = q_of_m m (γ L) → a = ps_monom c (- β L) → in_K_1_m a (m * q).
proof: Proof. intros f L m a c q HL Hm Hq Ha. constructor; subst a. remember (p_of_m m (γ L)) as p eqn:Hp . pose proof (any_is_p_mq (γ L) m Hp Hq) as Hgp. destruct Hgp as (Hgp, Hg). remember HL as Hini; clear HeqHini. apply exists_ini_pt_nat in Hini. destruct Hini as (j, (αj, Hini)). remember HL as Him; clear HeqHim. symmetry in Hini. eapply pol_ord_of_ini_pt in Him; eauto . remember HL as Hbm; clear HeqHbm. apply points_in_any_newton_segment with (h := Qnat j) (αh := αj) in Hbm. rewrite Him, Hgp in Hbm. remember (mh_of_m m αj (ps_poly_nth j f)) as mj. remember (mj * Zpos q + Z.of_nat j * p # m * q) as v. exists (ps_monom c (- v)); subst v; simpl. split; [ idtac | reflexivity ]. rewrite Hbm. unfold ps_monom; simpl. rewrite ps_adjust_eq with (n := O) (k := m). unfold adjust_ps; simpl. rewrite Z.sub_0_r. rewrite fold_series_const. rewrite series_stretch_const, series_shift_0. apply mkps_morphism; try reflexivity. rewrite Z.mul_opp_l; f_equal. rewrite Z.mul_add_distr_r; f_equal. rewrite <- Z.mul_assoc; f_equal. apply Z.mul_comm. apply Pos.mul_comm. left; symmetry; eassumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fpolynomial Newton Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base AlgCloCharPol PosOrder CharactPolyn ConvexHull PolyConvexHull F1Eq QbarM