proposition: Theorem root_tail_sep_1st_monom_any_r : ∀ f L f₁ L₁ c m q₀ n r, newton_segments f = Some L → pol_in_K_1_m f m → q₀ = q_of_m m (γ L) → c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → (∀ i, (i ≤ S n)%nat → (ps_poly_nth 0 (nth_pol i f L) ≠ 0)%ps) → (∀ i, i ≤ 1%nat → nth_r i f L = r) → (∀ i, r ≤ nth_r i f L) → (root_tail (m * q₀) n f₁ L₁ = ps_monom (nth_c n f₁ L₁) (nth_γ n f₁ L₁) + ps_monom 1%K (nth_γ n f₁ L₁) * root_tail (m * q₀) (S n) f₁ L₁)%ps.
proof: Proof. intros f L f₁ L₁ c m q₀ n r HL Hm Hq₀ Hc Hf₁ HL₁ Hpsi Hri Hrle. remember (zerop_1st_n_const_coeff (S n) f L) as z₁ eqn:Hz . symmetry in Hz. destruct z₁. apply zerop_1st_n_const_coeff_false_iff in Hpsi. rewrite Hpsi in Hz. discriminate Hz. assert (∀ i, i ≤ S n → nth_r i f L = r) as H. apply non_decr_imp_eq; auto with Arith. clear Hri; rename H into Hri; move Hri before Hrle. assert (∀ i, i ≤ n → (ps_poly_nth 0 (nth_pol i f₁ L₁) ≠ 0)%ps) as H. intros i Hin. apply Nat.succ_le_mono in Hin. apply Hpsi in Hin; simpl in Hin. rewrite <- Hc, <- Hf₁, <- HL₁ in Hin; assumption. rename H into Hpsi₁; move Hpsi₁ before Hpsi. assert (∀ j, r ≤ nth_r j f₁ L₁) as H. intros j. pose proof (Hrle (S j)) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H; assumption. rename H into Hrle₁; move Hrle₁ before Hrle. eapply root_tail_sep_1st_monom; eauto with Arith. 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