proposition: Theorem ps_monom_opp : ∀ c pow, (ps_monom (- c)%K pow = - ps_monom c pow)%ps.
proof: Proof. intros c pow. progress unfold ps_monom; simpl. progress unfold ps_opp; simpl. progress unfold series_opp; simpl. apply mkps_morphism; try reflexivity. constructor; intros i; simpl. destruct (zerop i); [ reflexivity | idtac ]. rewrite rng_opp_0; 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