proposition: Theorem a₀_neq_0 : ∀ f L αj, newton_segments f = Some L → ini_pt L = (Qnat 0, αj) → (ps_poly_nth 0 f ≠ 0)%ps.
proof: Proof. intros f L αj HL Hini. intros H₁. unfold ps_poly_nth, ps_lap_nth in H₁. remember HL as H; clear HeqH. remember (List.nth 0 (al f) 0%ps) as jps eqn:Hjps . eapply ord_coeff_non_zero_in_newt_segm with (hps := jps) in H; try eassumption . apply order_inf in H₁. unfold order in H₁; simpl in H₁. unfold order_coeff in H; simpl in H. remember (series_order (ps_terms jps) 0) as v eqn:Hv . destruct v as [v| ]. discriminate H₁. exfalso; apply H; reflexivity. left; symmetry; try eassumption; eauto with Arith. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail