proposition: Theorem ps_lap_in_power : ∀ la n, (∀ a, ps_lap_in a la → (order a ≥ 0)%Qbar) → (∀ m, ps_lap_in m (la ^ n) → (order m ≥ 0)%Qbar).
proof: Proof. intros la n Ha m Hm. revert m la Ha Hm. induction n; intros. simpl in Hm. destruct Hm as [(H₁, Hm)| ]; [ idtac | contradiction ]. rewrite <- Hm. apply ps_monom_order_ge. simpl in Hm. eapply ps_lap_in_mul_ge in Hm; try eassumption. intros p Hp. eapply IHn; eassumption. Qed.
imports: Utf8 QArith NPeano Sorted Misc NbarM QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHull ConvexHullMisc PolyConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq