proposition: Theorem order_inf : ∀ x, order x = qinf ↔ (x = 0)%ps.
proof: Proof. intros x. split; intros H. apply ps_series_order_inf_iff. unfold order in H. remember (series_order (ps_terms x) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]; [ discriminate H | reflexivity ]. apply ps_series_order_inf_iff in H. unfold order. rewrite H; reflexivity. Qed.
imports: Utf8 QArith Sorting ConvexHull ConvexHullMisc Misc NbarM QbarM Newton Field2 Fpolynomial Power_series Puiseux_series Ps_add Ps_add_compat Ps_mul Ps_div