proposition: Theorem root_head_from_cγ_list_succ_r : ∀ f L f₁ L₁ c n i, c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → zerop_1st_n_const_coeff n f₁ L₁ = false → (ps_poly_nth 0 f₁ ≠ 0)%ps → (root_head_from_cγ_list f L 0 n (S i) = ps_monom 1%K (γ L) * root_head_from_cγ_list f₁ L₁ 0 n i)%ps.
proof: Proof. intros f L f₁ L₁ c n i Hc Hf₁ HL₁ Hnz Hnz₁. revert f L f₁ L₁ c i Hc Hf₁ HL₁ Hnz Hnz₁. induction n; intros. simpl. unfold γ_sum; simpl. rewrite summation_split_first; [ idtac | apply Nat.le_0_l ]. rewrite summation_shift; [ idtac | apply le_n_S, Nat.le_0_l ]. rewrite Nat_sub_succ_1. do 2 rewrite rng_add_0_r; simpl. rewrite <- Hc, <- Hf₁, <- HL₁. rewrite rng_add_comm. rewrite ps_monom_add_r. apply ps_mul_comm. simpl in Hnz. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₁| H₁]. discriminate Hnz. remember (S i) as si; simpl. rewrite <- Hc, <- Hf₁, <- HL₁. subst si; simpl. rewrite <- Hc, <- Hf₁, <- HL₁. 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₂. unfold γ_sum; simpl. rewrite summation_split_first; [ idtac | apply Nat.le_0_l ]. rewrite summation_shift; [ idtac | apply le_n_S, Nat.le_0_l ]. rewrite Nat_sub_succ_1. destruct (ps_zerop K (ps_poly_nth 0 (nth_pol i f₂ L₂))) as [H₂| H₂]. do 2 rewrite rng_add_0_r. rewrite rng_add_comm. rewrite ps_monom_add_r; simpl. rewrite <- Hc, <- Hf₁, <- HL₁. apply ps_mul_comm. simpl. rewrite <- Hc, <- Hf₁, <- HL₁. rewrite ps_mul_add_distr_l. apply rng_add_compat. rewrite rng_add_comm; simpl. rewrite ps_monom_add_r. apply ps_mul_comm. apply IHn with (c := c); auto. rewrite zerop_1st_n_const_coeff_false_iff in Hnz. apply zerop_1st_n_const_coeff_false_iff. clear i H₂. intros i Hin. destruct i; [ assumption | simpl ]. rewrite <- Hc₁, <- Hf₂, <- HeqL₂. apply Hnz, Nat.lt_le_incl; 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