proposition: Theorem order_0 : order 0%ps = QbarM.qinf.
proof: Proof. unfold order; simpl. rewrite series_order_series_0; 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