proposition: Theorem zerop_1st_n_const_coeff_more : ∀ f L n, zerop_1st_n_const_coeff n f L = false → (ps_poly_nth 0 (nth_pol (S n) f L) ≠ 0)%ps → zerop_1st_n_const_coeff (S n) f L = false.
proof: Proof. intros f L n Hz Hn. rewrite zerop_1st_n_const_coeff_succ2. rewrite Hz, Bool.orb_false_l. remember (S n) as sn; simpl; subst sn. destruct (ps_zerop K (ps_poly_nth 0 (nth_pol (S n) f L))); auto with Arith. contradiction. 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