proposition: Theorem in_points_of_ps_lap_gen_lt : ∀ la pow pt, pt ∈ points_of_ps_lap_gen pow la → (nat_num (fst pt) < pow + length la)%nat.
proof: Proof. intros la pow pt Hpt. unfold points_of_ps_lap_gen in Hpt. destruct pt as (h, hv); simpl. eapply in_pts_in_ppl with (def := 0%ps) in Hpt; try reflexivity. destruct Hpt as (Hpt, Hord). eapply in_power_list_lt; eassumption. 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