proposition: Theorem nth_root_tail_const_plus_tail : ∀ f f₁ L L₁ Lb Lb₁ b r fb fb₁ αjb₂ αkb₂ m, newton_segments f₁ = Some L₁ → newton_segments fb = Some Lb → newton_segments fb₁ = Some Lb₁ → f₁ = next_pol f (β L) (γ L) (ac_root (Φq f L)) → fb = nth_pol b f L → fb₁ = next_pol fb (β Lb) (γ Lb) (ac_root (Φq fb Lb)) → L₁ = nth_ns 1 f L → Lb = nth_ns b f L → Lb₁ = option_get phony_ns (newton_segments fb₁) → (ps_poly_nth 0 fb ≠ 0)%ps → (ps_poly_nth 0 fb₁ ≠ 0)%ps → (∀ n, r ≤ nth_r n fb Lb) → root_multiplicity acf (ac_root (Φq fb Lb)) (Φq fb Lb) = r → root_multiplicity acf (ac_root (Φq fb₁ Lb₁)) (Φq fb₁ Lb₁) = r → pol_in_K_1_m fb m → pol_in_K_1_m fb₁ m → ini_pt Lb = (Qnat 0, αjb₂) → fin_pt Lb = (Qnat r, αkb₂) → (0 < Qnum αjb₂)%Z → Qnum αkb₂ = 0%Z → (series (root_tail_series_from_cγ_list m fb Lb) = series_const (nth_c b f L) + series_shift (Z.to_nat (p_of_m m (γ Lb₁))) (series (root_tail_series_from_cγ_list m fb₁ Lb₁)))%ser.
proof: Proof. intros f f₁ L L₁ Lb Lb₁ b r fb fb₁ αjb αkb m. intros HL₁i HLbi HLb₁i Hf₁ Hfb Hfb₁n. intros HL₁ HLb HLb₁₁ Hpsib Hpsib₁ Hrle Hrb Hrb₁ HKb HKb₁. intros Hinib Hfinb Hαjb Hαkb. simpl in HL₁; rewrite <- Hf₁ in HL₁. remember (ac_root (Φq f L)) as c₁ eqn:Hc₁. remember (ac_root (Φq fb₁ Lb₁)) as cb₃ eqn:Hcb₃. remember (p_of_m m (γ Lb)) as pb₂ eqn:Hpb₂. remember (p_of_m m (γ Lb₁)) as pb₃ eqn:Hpb₃. assert (Hfb₁ : fb₁ = nth_pol b f₁ L₁). rewrite Hfb₁n. symmetry. destruct b. simpl in Hfb, HLb; simpl. subst fb Lb c₁; assumption. apply nth_pol_succ. subst fb; simpl. rewrite <- Hc₁, <- Hf₁, <- HL₁; reflexivity. subst Lb; simpl. rewrite <- Hc₁, <- Hf₁, <- HL₁; reflexivity. symmetry. apply nth_c_n. subst fb; simpl. rewrite <- Hc₁, <- Hf₁, <- HL₁; reflexivity. subst Lb; simpl. rewrite <- Hc₁, <- Hf₁, <- HL₁; reflexivity. generalize HLbi; intros H. eapply next_ns_r_non_decr in H; try eassumption; try reflexivity. destruct H as (_, H). destruct H as (αjb₃, (αkb₃, H)). destruct H as (Hinib₃, (Hfinb₃, (Hαjb₃, Hαkb₃))). assert (Hpb₃pos : (0 < pb₃)%Z). subst pb₃. eapply p_is_pos; try eassumption. eapply multiplicity_is_pos; eassumption. constructor; simpl; intros i. destruct (zerop i) as [H₁| H₁]. subst i; simpl. destruct (lt_dec 0 (Z.to_nat pb₃)) as [H₁| H₁]. rewrite rng_add_0_r. unfold root_tail_series_from_cγ_list; simpl. destruct (ps_zerop K (ps_poly_nth 0 fb)) as [H₃| H₃]. contradiction . clear H₃; symmetry. erewrite nth_c_n; try eassumption; reflexivity. apply Nat.nlt_ge in H₁. apply Nat.le_0_r in H₁. rewrite <- Z2Nat.inj_0 in H₁. apply Z2Nat.inj in H₁. rewrite H₁ in Hpb₃pos. exfalso; revert Hpb₃pos; apply Z.lt_irrefl. apply Z.lt_le_incl; assumption. reflexivity. rewrite rng_add_0_l. destruct (lt_dec i (Z.to_nat pb₃)) as [H₂| H₂]. unfold root_tail_series_from_cγ_list; simpl. destruct i; [ exfalso; revert H₁; apply Nat.lt_irrefl | ]. clear H₁. rewrite <- Hfb₁n, <- HLb₁₁. destruct (ps_zerop K (ps_poly_nth 0 fb)) as [| H₁]; [ reflexivity | ]. simpl. destruct (ps_zerop K (ps_poly_nth 0 fb₁)) as [| H₃]; [ reflexivity | ]. clear H₁ H₃. erewrite next_pow_eq_p; try eassumption. rewrite <- Hpb₃. remember (Nat.compare (Z.to_nat pb₃) (S i)) as cmp eqn:Hcmp . symmetry in Hcmp. destruct cmp; [ | | reflexivity ]. apply nat_compare_eq in Hcmp. rewrite Hcmp in H₂. exfalso; revert H₂; apply Nat.lt_irrefl. apply nat_compare_lt in Hcmp. eapply Nat.lt_trans in H₂; eauto with Arith. exfalso; revert H₂; apply Nat.lt_irrefl. eapply multiplicity_is_pos; [ apply HLbi | reflexivity | assumption ]. apply Nat.nlt_ge in H₂. remember (i - Z.to_nat pb₃)%nat as id. unfold root_tail_series_from_cγ_list. remember Hinib as H; clear HeqH. symmetry in Hrb. eapply q_eq_1_any_r in H; try eassumption; try reflexivity. rename H into Hqb₂. remember Hinib₃ as H; clear HeqH. symmetry in Hrb₁. eapply q_eq_1_any_r in H; try eassumption; try reflexivity. rename H into Hqb₃. rewrite find_coeff_iter_succ with (r := r); auto with Arith; symmetry. rewrite Hcb₃ in Hrb₁. rewrite find_coeff_iter_succ with (r := r); auto with Arith. symmetry. remember (S i) as si. remember (S (S id)) as ssid; simpl. destruct i; [ exfalso; revert H₁; apply Nat.lt_irrefl | ]. clear H₁. destruct (ps_zerop K (ps_poly_nth 0 fb)); [ contradiction | ]. erewrite <- nth_pol_n with (c := c₁); eauto with Arith. rewrite <- Hfb₁, <- HLb₁₁. rewrite <- Hcb₃ in Hrb₁. symmetry in Hrb₁. erewrite next_pow_eq_p; try eassumption. rewrite <- Hpb₃. subst si ssid. remember (S i) as si. remember (S id) as sid; simpl. destruct (ps_zerop K (ps_poly_nth 0 fb₁)) as [| H₁]; auto with Arith. clear H₁. subst si. remember (Nat.compare (Z.to_nat pb₃) (S i)) as cmp₁. rename Heqcmp₁ into Hcmp₁. symmetry in Hcmp₁. destruct cmp₁. apply nat_compare_eq in Hcmp₁. rewrite Hcmp₁, Nat.sub_diag in Heqid; subst id; reflexivity. apply nat_compare_lt in Hcmp₁. destruct id. symmetry in Heqid. apply Nat.sub_gt in Heqid; try assumption. contradiction . rewrite <- Hcb₃. remember (next_pol fb₁ (β Lb₁) (γ Lb₁) cb₃) as fb₄. remember (option_get phony_ns (newton_segments fb₄)) as Lb₄. rename Heqfb₄ into Hfb₄. rename HeqLb₄ into HLb₄. subst sid. remember (Z.to_nat pb₃) as x. replace x with (0 + x)%nat by reflexivity. rewrite next_pow_add. replace (S i)%nat with (S i - x + x)%nat at 2 by (apply Nat.sub_add; assumption). rewrite find_coeff_add. rewrite <- Heqid. symmetry. destruct (ps_zerop K (ps_poly_nth 0 fb₄)) as [H₁| H₁]. remember (S id) as sid; simpl. destruct (ps_zerop K (ps_poly_nth 0 fb₄)) as [H₃| H₃]. reflexivity. contradiction . remember Hinib as H; clear HeqH. eapply p_is_pos with (m := m) in H; eauto with Arith. rewrite <- Hpb₂ in H. rename H into Hpb₂pos. remember HLb₁i as H; clear HeqH. eapply next_ns_in_f in H; eauto with Arith. rename H into HLb₄i. remember HLb₁i as H; clear HeqH. eapply nth_pol_in_K_1_m with (n := 1%nat) in H; eauto with Arith. simpl in H. rewrite <- Hcb₃, <- Hfb₄ in H. rename H into HK₄. remember HLb₁i as H; clear HeqH. eapply q_eq_1_r_non_decr in H; eauto with Arith. rename H into Hqb₄. remember (ac_root (Φq fb₄ Lb₄)) as cb₄ eqn:Hcb₄ . remember (root_multiplicity acf cb₄ (Φq fb₄ Lb₄)) as r₁ eqn:Hrb₄ . symmetry in Hrb₄. pose proof (Hrle 2%nat) as H. remember (S 0) as one in H; simpl in H. erewrite <- nth_pol_n with (c := c₁) in H; eauto with Arith. rewrite <- Hfb₁, <- HLb₁₁ in H. subst one; simpl in H. rewrite <- Hcb₃, <- Hfb₄, <- HLb₄, <- Hcb₄ in H. rewrite Hrb₄ in H. rename H into Hrr. eapply find_coeff_more_iter with (r := r); eauto with Arith. remember HLb₁i as H; clear HeqH. eapply next_ns_r_non_decr in H; eauto with Arith. destruct H as (HH, H); move H₁ at top; subst r₁. symmetry; assumption. intros j. pose proof (Hrle (j + 2)%nat) as H. rewrite nth_r_add in H. remember (S 0) as one in H; simpl in H. erewrite <- nth_pol_n with (c := c₁) in H; eauto with Arith. rewrite <- Hfb₁, <- HLb₁₁ in H. subst one; simpl in H. rewrite <- Hcb₃, <- Hfb₄, <- HLb₄ in H. assumption. subst x. apply Z2Nat.inj_lt in Hpb₃pos; try eassumption. rewrite Heqid. apply le_n_S. apply Nat.le_sub_le_add_l. apply Nat.le_sub_le_add_r. rewrite Nat_sub_succ_diag. assumption. reflexivity. apply Z.lt_le_incl; assumption. intros j; clear H. pose proof (Hrle (j + 1)%nat) as H. rewrite nth_r_add in H; simpl in H. erewrite <- nth_pol_n with (c := c₁) in H; try eassumption. rewrite <- Hfb₁, <- HLb₁₁ in H. assumption. reflexivity. intros j; clear H. pose proof (Hrle (j + 1)%nat) as H. rewrite nth_r_add in H; simpl in H. erewrite <- nth_pol_n with (c := c₁) in H; try eassumption. rewrite <- Hfb₁, <- HLb₁₁ in H; assumption. reflexivity. intros j Hj. destruct j; [ assumption | simpl ]. apply le_S_n in Hj. rewrite Nat.le_0_r in Hj; subst j. rewrite <- Hcb₃, <- Hfb₄, <- HLb₄. assumption. eapply multiplicity_is_pos; [ apply HLbi | reflexivity | ]. symmetry; assumption. apply nat_compare_gt, Nat.nle_gt in Hcmp₁. contradiction . eapply multiplicity_is_pos; [ apply HLbi | reflexivity | ]. symmetry; eassumption. intros j. pose proof (Hrle (j + 1)%nat) as H. rewrite nth_r_add in H; simpl in H. erewrite <- nth_pol_n with (c := c₁) in H; try eassumption. rewrite <- Hfb₁, <- HLb₁₁ in H; assumption. reflexivity. 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