proposition: Theorem zerop_1st_n_const_coeff_false_before : ∀ f L m, zerop_1st_n_const_coeff m f L = false → ∀ i, i ≤ m → zerop_1st_n_const_coeff i f L = false.
proof: Proof. intros f L m H i Hi. rewrite zerop_1st_n_const_coeff_false_iff in H. apply zerop_1st_n_const_coeff_false_iff. intros j Hj; apply H. transitivity i; assumption. 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