proposition: Theorem zerop_1st_n_const_coeff_succ : ∀ f L n, zerop_1st_n_const_coeff (S n) f L = zerop_1st_n_const_coeff 0 f L || zerop_1st_n_const_coeff n (nth_pol 1 f L) (nth_ns 1 f L).
proof: Proof. intros f L n; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); reflexivity. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM