proposition: Theorem not_zero_1st_prop : ∀ f L b, zerop_1st_n_const_coeff b (nth_pol 1 f L) (nth_ns 1 f L) = false → (ps_poly_nth 0 f ≠ 0)%ps → (∀ i, i ≤ S b → (ps_poly_nth 0 (nth_pol i f L) ≠ 0)%ps).
proof: Proof. intros f L b Hpsi Hnz. apply zerop_1st_n_const_coeff_false_iff. rewrite zerop_1st_n_const_coeff_succ. rewrite Hpsi, Bool.orb_false_r; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); [ contradiction | ]. reflexivity. 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