proposition: Theorem ps_monom_0_order : ∀ c n, (c = 0)%K → order (ps_monom c n) = qinf.
proof: Proof. intros c n Hc. unfold order. remember (series_order (ps_terms (ps_monom c n)) 0) as m eqn:Hm . symmetry in Hm. apply series_order_iff in Hm. simpl in Hm; simpl. destruct m as [m| ]; [ exfalso | reflexivity ]. destruct Hm as (Him, Hm). destruct m as [| m]; apply Hm; [ assumption | reflexivity ]. Qed.
imports: Utf8 QArith NPeano Sorted Misc NbarM QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHull ConvexHullMisc PolyConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq