proposition: Theorem fold_ps_lap_pow : ∀ α (R : ring α) (K : field R) a n, @lap_power _ (ps_ring K) a n = ps_lap_pow a n.
proof: Proof. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fpolynomial Puiseux_series Ps_add Ps_mul Ps_div