proposition: Theorem ps_lap_nth_0_cons_pow : ∀ a la n, (ps_lap_nth 0 ([a … la] ^ n) = a ^ n)%ps.
proof: Proof. intros a la n. induction n; simpl. progress unfold ps_lap_pow; simpl. reflexivity. unfold ps_lap_pow; simpl. unfold ps_lap_nth. rewrite list_nth_lap_mul; simpl. unfold summation; simpl. rewrite IHn. rewrite ps_add_0_r; 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