proposition: Theorem ps_monom_split_mul : ∀ c pow, (ps_monom c pow = ps_monom c 0 * ps_monom 1%K pow)%ps.
proof: Proof. intros c pow. rewrite <- ps_monom_add_r. rewrite Qplus_0_l; reflexivity. 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