proposition: Theorem apply_nth_pol : ∀ f L y n, let qr := Q_ring in zerop_1st_n_const_coeff n f L = false → (ps_pol_apply f (root_head 0 n f L + ps_monom 1%K (γ_sum 0 n f L) * y) = ps_monom 1%K (Σ (i = 0, n), β (nth_ns i f L)) * ps_pol_apply (nth_pol (S n) f L) y)%ps.
proof: Proof. intros; revert H; intros Hnz. revert f L y Hnz. induction n; intros. unfold root_head; simpl. unfold γ_sum, summation; simpl. unfold next_pol; simpl. unfold ps_pol_apply; simpl. unfold apply_poly; simpl. unfold next_lap; simpl. remember (ac_root (Φq f L)) as c eqn:Hc . rewrite apply_lap_mul; simpl. rewrite rng_mul_0_l, rng_add_0_l. symmetry; rewrite rng_add_0_r; symmetry. rewrite rng_mul_assoc; simpl. rewrite <- ps_monom_add_r. rewrite rng_add_opp_r; simpl. rewrite ps_mul_1_l. rewrite apply_lap_compose; simpl. rewrite rng_mul_0_l, rng_add_0_l. simpl in Hnz. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]. discriminate Hnz. do 2 rewrite rng_add_0_r. rewrite rng_add_comm; reflexivity. simpl in Hnz. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]. discriminate Hnz. 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. remember (S n) as sn in |- *; simpl. 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 ps_monom_add_r. rewrite <- rng_mul_assoc. subst sn; simpl. erewrite nth_pol_n with (f := f₁) (L := L₁); eauto . erewrite <- nth_pol_succ; eauto ; [ idtac | erewrite nth_c_n; eauto ]. remember (S n) as sn in |- *; simpl. unfold root_head; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₂| H₂]. contradiction. clear H₂. rewrite Heqsn in |- * at 1; simpl. rewrite <- Hc, <- Hf₁. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₂| H₂]. rewrite zerop_1st_n_const_coeff_false_iff in Hnz. pose proof (Hnz O (Nat.le_0_l n)) as H; contradiction. subst sn. rewrite <- IHn; auto. unfold root_head; simpl. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₃| H₃]. contradiction. clear H₃. unfold γ_sum at 1, summation; simpl. rewrite rng_add_0_r. unfold γ_sum. 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; simpl. rewrite <- Hc, <- Hf₁, <- HL₁. rewrite ps_monom_add_r. remember Σ (i = 0, n), nth_γ i f₁ L₁ as sγ eqn:Hsγ . rewrite <- ps_mul_assoc. remember (ps_monom 1%K sγ * y)%ps as u eqn:Hu . rewrite Hf₁ in |- * at 1; simpl. unfold next_pol; simpl. unfold ps_pol_apply; simpl. unfold apply_poly; simpl. unfold next_lap; simpl. rewrite apply_lap_mul; simpl. rewrite rng_mul_0_l, rng_add_0_l. rewrite rng_mul_assoc; simpl. rewrite <- ps_monom_add_r. rewrite rng_add_opp_r; simpl. rewrite ps_mul_1_l. rewrite apply_lap_compose; simpl. rewrite rng_mul_0_l, rng_add_0_l. symmetry; rewrite ps_add_comm; symmetry. rewrite ps_mul_add_distr_l. rewrite ps_add_assoc. rewrite root_head_from_cγ_list_succ_r; eauto . 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