proposition: Theorem ps_lap_nth_0_apply_0 : ∀ la, (ps_lap_nth 0 la = @apply_lap _ (ps_ring K) la 0)%ps.
proof: Proof. intros la. induction la as [| a]; [ reflexivity | simpl ]. rewrite ps_mul_0_r, ps_add_0_l. reflexivity. 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