proposition: Theorem nth_root_tail_const : ∀ f L f₁ L₁ n fn Ln fn₁ Ln₁ c m, c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → fn = nth_pol n f L → Ln = nth_ns n f L → (ps_poly_nth 0 fn ≠ 0)%ps → fn₁ = nth_pol n f₁ L₁ → Ln₁ = nth_ns n f₁ L₁ → (ps_poly_nth 0 fn₁ = 0)%ps → ({| terms := root_tail_series_from_cγ_list m fn Ln |} = series_const (nth_c n f L))%ser.
proof: Proof. intros f₁ L₁ f₂ L₂ b₁ fb₂ Lb₂ fb₁ Lb₁ c₁ m₁. intros Hc₁ Hf₂ HL₂ Hfb₂ HLb₂ Hpsib₁ Hfb₁ HLb₁ H₁. constructor; intros i; simpl. rename H₁ into Hzb₃. destruct (zerop i) as [H₁| H₁]. subst i; simpl. unfold root_tail_series_from_cγ_list; simpl. destruct (ps_zerop K (ps_poly_nth 0 fb₂)) as [| H₁]; [ contradiction | ]. erewrite nth_c_n; try eassumption; reflexivity. unfold root_tail_series_from_cγ_list; simpl. destruct (ps_zerop K (ps_poly_nth 0 fb₂)) as [| H₂]; [ contradiction | ]. destruct i; [ exfalso; revert H₁; apply Nat.lt_irrefl | ]. remember (ac_root (Φq fb₂ Lb₂)) as cb₂ eqn:Hcb₂ . erewrite <- nth_pol_n with (c := c₁); try eassumption. erewrite <- nth_ns_n with (c := c₁); try eassumption. simpl; rewrite <- Hfb₁. destruct (ps_zerop K (ps_poly_nth 0 fb₁)); [ | contradiction ]. reflexivity. eapply nth_pol_n with (c := c₁); eassumption. 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