proposition: Theorem root_head_from_cγ_list_succ : ∀ f L b n i, zerop_1st_n_const_coeff (b + i) f L = false → (root_head_from_cγ_list f L b (S n) i = root_head_from_cγ_list f L b n i + (if zerop_1st_n_const_coeff (b + i + S n) f L then 0 else ps_monom (nth_c (b + i + S n) f L) (γ_sum b (i + S n) f L)))%ps.
proof: Proof. intros f L b n i Hz; simpl. revert b i Hz. induction n; intros; simpl. symmetry; rewrite rng_add_0_r; symmetry. rewrite Nat.add_1_r. remember (zerop_1st_n_const_coeff (S (b + i)) f L) as z₁ eqn:Hz₁ . symmetry in Hz₁. rewrite Nat.add_succ_r. destruct z₁. rewrite zerop_1st_n_const_coeff_succ2 in Hz₁. rewrite Hz, Bool.orb_false_l in Hz₁. remember (nth_pol (S (b + i)) f L) as p. simpl in Hz₁. destruct (ps_zerop K (ps_poly_nth 0 p)) as [H₂| H₂]; subst p. reflexivity. discriminate Hz₁. apply zerop_1st_n_const_coeff_false_iff with (i := S (b + i)) in Hz₁. remember (nth_pol (S (b + i)) f L) as p. destruct (ps_zerop K (ps_poly_nth 0 p)) as [H₂| H₂]; subst p. contradiction. rewrite rng_add_0_r, Nat.add_1_r; reflexivity. reflexivity. rewrite <- rng_add_assoc; simpl. apply rng_add_compat_l; simpl. remember (nth_pol (b + S i) f L) as p. destruct (ps_zerop K (ps_poly_nth 0 p)) as [H₁| H₁]; subst p. rewrite rng_add_0_l. remember (zerop_1st_n_const_coeff (b + i + S (S n)) f L) as z₁ eqn:Hz₁ . symmetry in Hz₁. destruct z₁; [ reflexivity | idtac ]. rewrite zerop_1st_n_const_coeff_false_iff in Hz₁. assert (b + S i ≤ b + i + S (S n)) as H by fast_omega . apply Hz₁ in H; contradiction. rewrite IHn. do 7 rewrite Nat.add_succ_r; rewrite Nat.add_succ_l. reflexivity. rewrite Nat.add_succ_r. rewrite zerop_1st_n_const_coeff_succ2. rewrite Hz, Bool.orb_false_l. rewrite <- Nat.add_succ_r. apply zerop_1st_n_const_coeff_false_iff. intros j Hj. apply Nat.le_0_r in Hj; subst j. 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