proposition: Theorem root_head_succ : ∀ f L b n, zerop_1st_n_const_coeff b f L = false → (root_head b (S n) f L = root_head b n f L + if zerop_1st_n_const_coeff (b + S n) f L then 0 else ps_monom (nth_c (b + S n) f L) (γ_sum b (S n) f L))%ps.
proof: Proof. intros f L b n Hz. unfold root_head; rewrite Hz. rewrite root_head_from_cγ_list_succ. rewrite Nat.add_0_r, Nat.add_0_l. reflexivity. rewrite Nat.add_0_r; assumption. 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