proposition: Theorem poly_inject_inj_mul : ∀ P Q, (poly_inject_K_in_Kx (P * Q)%pol = (poly_inject_K_in_Kx P * poly_inject_K_in_Kx Q))%pspol.
proof: Proof. intros P Q. 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