proposition: Theorem zerop_1st_n_const_coeff_true_if : ∀ f L b, zerop_1st_n_const_coeff b f L = true → ∀ n, zerop_1st_n_const_coeff (b + n) f L = true.
proof: Proof. intros f L b Hz n. revert f L Hz n. induction b; intros. simpl. revert f L Hz. induction n; intros; auto. simpl in Hz; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); auto. discriminate Hz. simpl in Hz; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); auto. 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