proposition: Theorem next_pol_in_K_1_mq : ∀ f f₁ L m c q, newton_segments f = Some L → pol_in_K_1_m f m → c = ac_root (Φq f L) → q = q_of_m m (γ L) → f₁ = next_pol f (β L) (γ L) c → pol_in_K_1_m f₁ (m * q).
proof: Proof. intros f f₁ L m c q HL Hm Hc Hq Hf₁. subst f₁. unfold next_pol, next_lap; simpl. apply ps_lap_forall_forall. intros a b Hab Hamq. rewrite <- Hab; assumption. intros b Hin. eapply in_K_1_m_lap_mul_compat; eauto . intros a Ha. destruct Ha as [Ha| ]; [ idtac | contradiction ]. destruct Ha as (_, Ha). rewrite <- Ha. eapply minus_beta_in_K_1_mq; eauto . intros ps Hps. eapply in_K_1_m_lap_comp_compat; eauto . intros a Ha. apply in_K_1_m_lap_mul_r_compat. revert a Ha. apply ps_lap_forall_forall. intros a d Hab Hamq. rewrite <- Hab; assumption. assumption. intros a Ha; simpl in Ha. destruct Ha as [Ha| [Ha| ]]; [ idtac | idtac | contradiction ]. destruct Ha as (Hla, Ha). symmetry in Ha. eapply gamma_in_K_1_mq; eassumption. destruct Ha as (Hla, Ha). symmetry in Ha. eapply gamma_in_K_1_mq; 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