proposition: Theorem order_fin : ∀ x, order x ≠ qinf ↔ (x ≠ 0)%ps.
proof: Proof. intros x. split; intros H I; apply H, order_inf; assumption. 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