proposition: Theorem ps_lap_nilp : ∀ la : list (puiseux_series α), {@lap_eq _ (ps_ring K) la []} + {not (@lap_eq _ (ps_ring K) la [])}.
proof: Proof. intros la. induction la as [| a]; [ left; reflexivity | idtac ]. destruct IHla as [IHla| IHla]. destruct (ps_zerop _ a) as [Ha| Ha]. left. rewrite IHla, Ha. constructor; reflexivity. right. intros H; apply Ha. apply lap_eq_cons_nil_inv in H. destruct H; assumption. right. intros H; apply IHla. apply lap_eq_cons_nil_inv in H. destruct H; assumption. 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