proposition: Theorem any_in_K_1_m : ∀ la m h αh, ps_lap_forall (λ a, in_K_1_m a m) la → (Qnat h, αh) ∈ points_of_ps_lap la → ∃ mh, αh == mh # m.
proof: Proof. intros la m h αh HinK Hin. unfold points_of_ps_lap in Hin. unfold points_of_ps_lap_gen in Hin. unfold qpower_list in Hin. remember O as pow; clear Heqpow. revert pow Hin. induction la as [| a]; intros; [ contradiction | idtac ]. simpl in Hin. inversion_clear HinK. apply lap_eq_cons_nil_inv in H. destruct H as (Ha, Hla); simpl in Ha. apply order_inf in Ha. rewrite Ha in Hin. eapply IHla; eauto . constructor; assumption. remember (order a) as v eqn:Hv . symmetry in Hv. destruct v as [v| ]. simpl in Hin. destruct Hin as [Hin| Hin]. injection Hin; clear Hin; intros; subst v. eapply in_K_1_m_order_eq; eauto . eapply IHla; eauto . eapply IHla; eauto . Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base