proposition: Theorem lap_power_map_ps : ∀ la n, (lap_inject_K_in_Kx la ^ n = lap_inject_K_in_Kx (la ^ n)%lap)%pslap.
proof: Proof. intros la n. unfold ps_lap_eq, ps_lap_pow. revert la. induction n; intros; [ reflexivity | simpl ]. rewrite IHn; symmetry. apply lap_mul_map_ps. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol