proposition: Theorem root_tail_when_r_r : ∀ f L f₁ L₁ m q₀ b r n, newton_segments f = Some L → pol_in_K_1_m f m → q₀ = q_of_m m (γ L) → f₁ = next_pol f (β L) (γ L) (ac_root (Φq f L)) → L₁ = option_get phony_ns (newton_segments f₁) → (∀ i, i ≤ 1%nat → nth_r i f L = r) → (∀ n, r ≤ nth_r n f L) → zerop_1st_n_const_coeff (S n) f L = false → (root_tail (m * q₀) b f₁ L₁ = root_head b n f₁ L₁ + ps_monom 1%K (γ_sum b n f₁ L₁) * root_tail (m * q₀) (b + S n) f₁ L₁)%ps.
proof: Proof. intros f L f₁ L₁ m q₀ b r n. intros HL Hm Hq₀ Hf₁ HL₁ Hri Hrle Hnz. remember (ac_root (Φq f L)) as c eqn:Hc. revert f L f₁ L₁ c m q₀ b HL Hm Hq₀ Hc Hf₁ HL₁ Hri Hrle Hnz. induction n; intros. unfold root_head; simpl. remember (zerop_1st_n_const_coeff b f₁ L₁) as z₁ eqn:Hz₁ . symmetry in Hz₁. destruct z₁. rewrite rng_add_0_l. unfold root_tail. rewrite Hz₁, Nat.add_1_r. rewrite zerop_1st_n_const_coeff_succ2. rewrite Hz₁, Bool.orb_true_l. rewrite rng_mul_0_r; reflexivity. rewrite Nat.add_0_r, rng_add_0_r. rewrite root_tail_from_0_const_r; try eassumption; auto with Arith. unfold root_head. rewrite Hz₁. unfold root_head_from_cγ_list. rewrite Nat.add_0_r, rng_add_0_r. rewrite Nat.add_1_r; reflexivity. remember (zerop_1st_n_const_coeff b f₁ L₁) as z₁ eqn:Hz₁ . symmetry in Hz₁. destruct z₁. unfold root_head, root_tail. rewrite Hz₁. rewrite zerop_1st_n_const_coeff_true_if; auto with Arith. rewrite rng_add_0_l, rng_mul_0_r; reflexivity. rewrite root_head_succ; auto with Arith. remember (zerop_1st_n_const_coeff (b + S n) f₁ L₁) as z eqn:Hz . symmetry in Hz. destruct z. rewrite rng_add_0_r, Nat.add_succ_r. rewrite IHn; try eassumption. apply rng_add_compat_l. unfold γ_sum at 2; simpl. rewrite summation_split_last; [ idtac | apply Nat.le_0_l ]. rewrite fold_γ_sum, ps_monom_add_r. rewrite <- rng_mul_assoc. apply rng_mul_compat_l. unfold root_tail. rewrite Hz. remember (b + S n)%nat as x; rewrite <- Nat.add_1_r; subst x. rewrite zerop_1st_n_const_coeff_true_if; auto with Arith. rewrite rng_mul_0_r; reflexivity. rewrite zerop_1st_n_const_coeff_succ2 in Hnz. apply Bool.orb_false_iff in Hnz. destruct Hnz; assumption. rewrite IHn; try eassumption. rewrite <- rng_add_assoc. apply rng_add_compat_l; simpl. symmetry. rewrite ps_monom_split_mul. rewrite rng_mul_comm, <- rng_mul_add_distr_l. unfold γ_sum at 1; simpl. rewrite summation_split_last; [ idtac | apply Nat.le_0_l ]. rewrite fold_γ_sum, ps_monom_add_r. rewrite <- rng_mul_assoc. apply rng_mul_compat_l. rewrite rng_mul_add_distr_l. rewrite rng_mul_comm; simpl. rewrite <- ps_monom_split_mul. symmetry. do 3 rewrite Nat.add_succ_r. eapply root_tail_sep_1st_monom_any_r; try eassumption. rewrite <- Nat.add_succ_r. apply zerop_1st_n_const_coeff_false_iff. rewrite zerop_1st_n_const_coeff_succ; simpl. rewrite <- Hc, <- Hf₁, <- HL₁. rewrite Hz; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]; auto with Arith. rewrite zerop_1st_n_const_coeff_false_iff in Hnz. pose proof (Hnz O (Nat.le_0_l (S (S n)))) as H. contradiction. rewrite zerop_1st_n_const_coeff_succ2 in Hnz. apply Bool.orb_false_iff in Hnz. destruct Hnz; assumption. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail