proposition: Theorem coeff_of_hl_eq_order : ∀ h la li, h ∈ li → coeff_of_hl K la h li = order_coeff (List.nth h la 0%ps).
proof: Proof. intros h la li Hh. induction li as [| i]; [ contradiction | simpl ]. destruct (eq_nat_dec h i) as [| Hhi]; [ subst; reflexivity | idtac ]. apply IHli. apply Nat.neq_sym in Hhi. destruct Hh as [Hh| ]; [ contradiction | 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