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