proposition: Theorem list_in_ps_lap_in : ∀ a l, (a ≠ 0)%ps → a ∈ l → ps_lap_in a l.
proof: Proof. intros a l Ha Hal. revert a Ha Hal. induction l as [| x]; intros; [ assumption | idtac ]. destruct Hal as [Hal| Hal]. subst a; left; split; [ idtac | reflexivity ]. intros H. apply lap_eq_cons_nil_inv in H. destruct H; contradiction. right; apply IHl; 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