proposition: Theorem degree_pos_imp_L_not_empty : ∀ f, degree (ps_zerop K) f ≥ 1 → (ps_poly_nth 0 f ≠ 0)%ps → newton_segments f ≠ None.
proof: Proof. intros f Hdeg Hnz. unfold degree in Hdeg. unfold ps_poly_nth in Hnz. unfold ps_lap_nth in Hnz. unfold newton_segments, points_of_ps_polynom. unfold points_of_ps_lap, points_of_ps_lap_gen; simpl. intros HLl. remember (al f) as la eqn:Hla . clear f Hla. destruct la as [| a]; [ apply Hnz; reflexivity | idtac ]. simpl in Hdeg, Hnz, HLl. remember (degree_plus_1_of_list (ps_zerop K) la) as d eqn:Hd . symmetry in Hd. destruct d. destruct (ps_zerop K a) as [H₁| H₁]. apply Nat.nlt_ge in Hdeg; apply Hdeg, Nat.lt_0_1. apply Nat.nlt_ge in Hdeg; apply Hdeg, Nat.lt_0_1. clear Hdeg. apply order_fin in Hnz. remember (order a) as va eqn:Hva . symmetry in Hva. destruct va as [va| ]; [ clear Hnz | apply Hnz; reflexivity ]. remember 1%nat as pow in HLl; clear Heqpow. revert a d va pow Hd Hva HLl. induction la as [| b]; intros; [ discriminate Hd | idtac ]. simpl in Hd. remember (degree_plus_1_of_list (ps_zerop K) la) as e eqn:He in Hd. symmetry in He. destruct e. destruct (ps_zerop K b) as [H₁| H₁]; [ discriminate Hd | idtac ]. clear d Hd. simpl in HLl. apply order_fin in H₁. remember (order b) as vb eqn:Hvb . symmetry in Hvb. destruct vb as [vb| ]; [ discriminate HLl | apply H₁; reflexivity ]. clear d Hd. simpl in HLl. remember (order b) as vb eqn:Hvb . symmetry in Hvb. destruct vb as [vb| ]; [ discriminate HLl | idtac ]. eapply IHla; eauto . 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 RootAnyR