proposition: Theorem ps_monom_order_ge : ∀ c n, (order (ps_monom c n) ≥ qfin n)%Qbar.
proof: Proof. intros c n. unfold order. remember (series_order (ps_terms (ps_monom c n)) 0) as m eqn:Hm . symmetry in Hm. unfold Qbar.ge. destruct m as [m| ]; [ idtac | constructor ]. apply Qbar.le_qfin. apply series_order_iff in Hm. simpl in Hm; simpl. destruct Hm as (Him, Hm). destruct m as [| m]; [ simpl | exfalso; apply Hm; reflexivity ]. simpl in Hm. rewrite Z.add_0_r; destruct n; simpl. unfold Qle; simpl; 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