proposition: Theorem zerop_1st_n_const_coeff_succ2 : ∀ f L n, zerop_1st_n_const_coeff (S n) f L = zerop_1st_n_const_coeff n f L || zerop_1st_n_const_coeff 0 (nth_pol (S n) f L) (nth_ns (S n) f L).
proof: Proof. intros f L n. revert f L. induction n; intros. simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); reflexivity. remember (S n) as sn; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]. rewrite Heqsn in |- * at 1; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); [ | contradiction ]. symmetry; apply Bool.orb_true_l. remember (ac_root (Φq f L)) as c₁ eqn:Hc₁ . remember (next_pol f (β L) (γ L) c₁) as f₁ eqn:Hf₁ . remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁ . rewrite IHn; simpl. remember (nth_pol sn f₁ L₁) as fn eqn:Hfn . destruct (ps_zerop K (ps_poly_nth 0 fn)) as [H₂| H₂]. do 2 rewrite Bool.orb_true_r; reflexivity. do 2 rewrite Bool.orb_false_r. subst sn; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)); [ contradiction | ]; subst; 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