proposition: Theorem order_nth_inject_K : ∀ la i, (0 ≤ order (ps_lap_nth i (lap_inject_K_in_Kx la)))%Qbar.
proof: Proof. intros la i. revert i. induction la as [| a]; intros; simpl. unfold ps_lap_nth. rewrite list_nth_nil. rewrite order_0; constructor. destruct i; [ idtac | apply IHla ]. unfold ps_lap_nth; simpl. apply ps_monom_order_ge. 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