proposition: Theorem ps_zerop : ∀ a, {(a = 0)%ps} + {(a ≠ 0)%ps}.
proof: Proof. intros a. destruct (Qbar.eq_dec (order a) QbarM.qinf) as [H| H]. left. apply order_inf. unfold Qbar.qeq in H. destruct (order a); [ contradiction | reflexivity ]. right. intros HH; apply H. apply order_inf in HH. rewrite HH; 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