proposition: Theorem root_tail_from_0_const_r : ∀ f L c f₁ L₁ c₁ m q₀ b 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₁) → c₁ = ac_root (Φq f₁ L₁) → (∀ i, i ≤ 1%nat → nth_r i f L = r) → (∀ n, r ≤ nth_r n f L) → (root_tail (m * q₀) b f₁ L₁ = root_head b 0 f₁ L₁ + ps_monom 1%K (γ_sum b 0 f₁ L₁) * root_tail (m * q₀) (S b) f₁ L₁)%ps.
proof: Proof. intros f L c f₁ L₁ c₁ m q₀ b r. intros HL Hm Hq₀ Hc Hf₁ HL₁ Hc₁ Hri Hrle. destruct b; [ eapply root_tail_split_1st_any_r; eassumption | ]. remember (zerop_1st_n_const_coeff (S b) f₁ L₁) as z₁ eqn:Hz₁ . symmetry in Hz₁. destruct z₁. unfold root_tail, root_head. rewrite Hz₁. rewrite zerop_1st_n_const_coeff_succ2. rewrite Hz₁; simpl. rewrite rng_add_0_l, rng_mul_0_r; reflexivity. remember (next_pol f₁ (β L₁) (γ L₁) c₁) as f₂ eqn:Hf₂ . remember (option_get phony_ns (newton_segments f₂)) as L₂ eqn:HL₂ . assert (Hain : ∀ n, n ≤ S b → newton_segments (nth_pol n f₁ L₁) = Some (nth_ns n f₁ L₁)). subst c; eapply not_zerop_imp_in_newton_segment; eassumption. rewrite zerop_1st_n_const_coeff_succ in Hz₁. apply Bool.orb_false_iff in Hz₁. destruct Hz₁ as (Hz₁, Hpsi). simpl in Hz₁. remember (ps_poly_nth 0 f₁) as y. destruct (ps_zerop K y) as [| Hnz₁]; [ discriminate Hz₁ | subst y ]. clear Hz₁. assert (Hreq : ∀ n, n ≤ S b → nth_r n f₁ L₁ = r). subst c; eapply not_zerop_imp_nth_r_eq_r; eassumption. assert (∀ i, i ≤ S b → (ps_poly_nth 0 (nth_pol i f₁ L₁) ≠ 0)%ps). apply not_zero_1st_prop; assumption. clear Hpsi; rename H into Hpsi. pose proof (Hpsi (S b) (Nat.le_refl (S b))) as H. rename H into Hpsib₁. remember (S b) as b₁ eqn:Hb₁ . remember (nth_ns b₁ f₁ L₁) as Lb eqn:HLb . remember (nth_pol b₁ f₁ L₁) as fb eqn:Hfb . pose proof (Hain b₁ (Nat.le_refl b₁)) as H. rewrite <- HLb, <- Hfb in H. rename H into HLbi. generalize Hf₁; intros H. eapply r_n_nth_ns with (r := r) in H; try eassumption. destruct H as (αjb₂, (αkb₂, H)). destruct H as (Hinib₂, (Hfinb₂, (Hαjb₂, Hαkb₂))). unfold root_tail, root_head. apply zerop_1st_n_const_coeff_false_iff in Hpsi. rewrite Hpsi. rewrite zerop_1st_n_const_coeff_succ2. rewrite Hpsi. rewrite zerop_1st_n_const_coeff_false_iff in Hpsi. simpl. rewrite <- Hc₁, <- Hf₂, <- HL₂. rewrite <- Hfb, <- HLb. rewrite Nat.add_0_r, rng_add_0_r. unfold root_tail_from_cγ_list, ps_monom; simpl. rewrite Nat.add_0_r, Z.mul_1_r, Z.add_0_r. rewrite Pos.mul_1_r. erewrite nth_γ_n; eauto with Arith; simpl. remember (nth_pol b₁ f₂ L₂) as fb₁ eqn:Hfb₁ . remember (nth_ns b₁ f₂ L₂) as Lb₁ eqn:HLb₁ . rewrite Hinib₂, Hfinb₂; simpl. rewrite Hαkb₂; simpl. rewrite Qnum_inv_Qnat_sub; [ | eapply multiplicity_pos; eassumption ]. rewrite Qden_inv_Qnat_sub; [ | eapply multiplicity_pos; eassumption ]. rewrite Z.add_0_r, Z.mul_1_r, Nat.sub_0_r. remember (m * q₀)%positive as m₁. rewrite Z.mul_shuffle0, Pos_mul_shuffle0. rewrite Pos2Z.inj_mul. rewrite Z.div_mul_cancel_r; try eassumption; try apply Pos2Z_ne_0. generalize HL₁; intros H. eapply r_n_next_ns with (L := L) in H; try eassumption. destruct H as (αj₁, (αk₁, H)). destruct H as (Hini₁, (Hfin₁, (Hαj₁, Hαk₁))). assert (H : newton_segments f₁ = Some L₁). eapply next_ns_in_f with (f := f); eassumption. eapply nth_pol_in_K_1_m with (fn := fb) in H; eauto with Arith. rename H into HKb₂. pose proof (Hreq b₁ (Nat.le_refl b₁)) as H. erewrite nth_r_n in H; eauto with Arith. erewrite nth_c_n in H; eauto with Arith. rename H into Hrb₂. erewrite αj_m_eq_p_r with (f₁ := fb); eauto with Arith. rewrite Pos2Z.inj_mul, Z.mul_shuffle0, Zposnat2Znat; auto with Arith. rewrite <- Z.mul_assoc. rewrite <- Zposnat2Znat; simpl; try eassumption. rewrite Z.div_mul; auto with Arith. destruct (ps_zerop K (ps_poly_nth 0 fb₁)) as [H₁| H₁]. rewrite rng_mul_0_r, rng_add_0_r. remember (Qden αjb₂ * Pos.of_nat r * Qden αkb₂)%positive as dd. rewrite ps_adjust_eq with (n := O) (k := dd); symmetry. rewrite ps_adjust_eq with (n := O) (k := m₁); symmetry. unfold adjust_ps; simpl. rewrite Pos.mul_comm. do 2 rewrite Z.sub_0_r. do 2 rewrite series_shift_0. rewrite fold_series_const, series_stretch_const. rewrite Z.mul_shuffle0. erewrite αj_m_eq_p_r with (f₁ := fb); try eassumption; eauto with Arith. do 2 rewrite <- Z.mul_assoc. remember (Z.of_nat r * (Zpos (Qden αjb₂) * Zpos (Qden αkb₂)))%Z as x. rewrite Z.mul_comm, Z.mul_shuffle0 in Heqx. rewrite <- Zposnat2Znat in Heqx; auto with Arith. simpl in Heqx. rewrite <- Heqdd in Heqx; subst x. apply mkps_morphism; auto with Arith. apply series_stretch_iff_const. eapply nth_root_tail_const; eassumption. eapply multiplicity_pos; eassumption. do 2 rewrite fold_series_const. assert (H : 1 ≤ b₁) by (subst b₁; apply le_n_S, Nat.le_0_l). apply Hain in H; simpl in H. rewrite <- Hc₁, <- Hf₂, <- HL₂ in H. rename H into HL₂i. clear q₀ Hq₀ Heqm₁. clear Hpsi Hreq. clear αj₁ αk₁ Hαj₁ Hαk₁ Hini₁ Hfin₁. clear Hnz₁ Hm Hain Hb₁ b. assert (Hrle₁ : ∀ i, r ≤ nth_r i f₁ L₁). eapply all_r_le_next with (L := L); eassumption. clear Hrle Hf₁ HL₁ Hc. revert HL HL₂i HLbi Hf₂ Hfb Hfb₁ HL₂ HLb HLb₁ Hpsib₁ H₁ Hrle₁ Hri Hrb₂ HKb₂ Hc₁ Hinib₂ Hfinb₂ Hαjb₂ Hαkb₂; clear; intros. rename H₁ into Hnzb₃. remember HLb₁ as H; clear HeqH. erewrite nth_ns_n in H; eauto with Arith. erewrite <- nth_pol_n in H; eauto with Arith. rewrite <- Hfb₁ in H. rename H into HLb₁₁. remember Hfb₁ as H; clear HeqH. erewrite nth_pol_n in H; eauto with Arith. rename H into Hfb₁n. remember HLb₁₁ as H; clear HeqH. eapply next_ns_in_f with (f := fb) in H; eauto with Arith. rename H into HLb₁i. pose proof (Hrle₁ (S b₁)) as H; simpl in H. rewrite <- Hc₁, <- Hf₂, <- HL₂ in H. rename H into Hler₃. remember HLbi as H; clear HeqH. remember (ac_root (Φq fb₁ Lb₁)) as cb₃ eqn:Hcb₃ . remember (root_multiplicity acf cb₃ (Φq fb₁ Lb₁)) as rcb₃ eqn:Hrcb₃ . symmetry in Hrcb₃. erewrite nth_r_n in Hler₃; eauto with Arith. erewrite nth_c_n in Hler₃; eauto with Arith. rewrite <- Hcb₃, Hrcb₃ in Hler₃. eapply next_ns_r_non_decr in H; eauto with Arith. destruct H as (H₁, H); move H₁ at top; subst rcb₃. destruct H as (αjb₃, (αkb₃, H)). destruct H as (Hinib₃, (Hfinb₃, (Hαjb₃, Hαkb₃))). rewrite Hinib₃, Hfinb₃; simpl. rewrite Hαkb₃; simpl. rewrite Qnum_inv_Qnat_sub; [ | eapply multiplicity_pos; eassumption ]. rewrite Qden_inv_Qnat_sub; [ | eapply multiplicity_pos; eassumption ]. rewrite Nat.sub_0_r. rewrite Z.add_0_r, Z.mul_1_r. remember (Qden αjb₂ * Pos.of_nat r * Qden αkb₂)%positive as dd. rewrite Z.mul_shuffle0, Pos_mul_shuffle0. do 2 rewrite Pos2Z.inj_mul. rewrite Z.div_mul_cancel_r; simpl; auto with Arith. remember (Qnum αjb₂ * Zpos (Qden αkb₂))%Z as nd. assert (Hrle₂ : ∀ n, r ≤ nth_r n fb Lb). intros i. pose proof (Hrle₁ (i + b₁)%nat) as H. rewrite nth_r_add in H. rewrite <- Hfb, <- HLb in H; assumption. remember HLbi as H; clear HeqH. eapply nth_pol_in_K_1_m with (n := 1%nat) in H; eauto with Arith. rename H into HKb₃. erewrite αj_m_eq_p_r with (f₁ := fb₁); try eassumption; eauto with Arith. rewrite Z.mul_shuffle0. rewrite <- Zposnat2Znat; auto with Arith. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul. rewrite Z.div_mul; auto with Arith. unfold ps_add, ps_mul; simpl. unfold cm; simpl. unfold ps_terms_add; simpl. unfold ps_ordnum_add; simpl. rewrite Z.mul_add_distr_r. rewrite Pos2Z.inj_mul, Z.mul_assoc, Z.mul_shuffle0. remember (nd * Zpos m₁ * Zpos dd)%Z as x. remember (p_of_m m₁ (γ Lb₁)) as pb₃ eqn:Hpb₃ . 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. assert (Hle : (x <= x + pb₃ * Zpos dd * Zpos dd)%Z). apply Z.le_sub_le_add_l. rewrite Z.sub_diag. apply Z.mul_nonneg_nonneg; auto with Arith. apply Z.mul_nonneg_nonneg; auto with Arith. apply Z.lt_le_incl; assumption. rewrite Z.min_l; auto with Arith. rewrite Z.min_r; auto with Arith. rewrite Z.add_simpl_l, Z.sub_diag; simpl. rewrite Pos.mul_assoc. rewrite ps_adjust_eq with (n := O) (k := (dd * dd)%positive). unfold adjust_ps; simpl. rewrite series_shift_0. rewrite Z.sub_0_r. subst nd x. remember (Qnum αjb₂ * Zpos (Qden αkb₂) * Zpos m₁)%Z as x. rewrite Z.mul_shuffle0 in Heqx; subst x. erewrite αj_m_eq_p_r with (L₁ := Lb) (f₁ := fb); eauto with Arith. remember (p_of_m m₁ (γ Lb)) as pb₂ eqn:Hpb₂ . remember (pb₂ * Z.of_nat r * Zpos (Qden αjb₂) * Zpos (Qden αkb₂))%Z as x. do 2 rewrite <- Z.mul_assoc in Heqx. rewrite Z.mul_comm, Z.mul_assoc in Heqx. remember (Z.of_nat r * Zpos (Qden αjb₂) * Zpos (Qden αkb₂))%Z as y eqn:Hy . rewrite Z.mul_comm in Heqx; subst x. rewrite Z.mul_shuffle0, Z.mul_comm in Hy. rewrite Z.mul_assoc in Hy. rewrite <- Zposnat2Znat in Hy; auto with Arith. simpl in Hy; rewrite <- Heqdd in Hy; subst y. remember (m₁ * (dd * dd))%positive as x. rewrite Pos.mul_comm in Heqx; subst x. rewrite Pos2Z.inj_mul, Z.mul_assoc. apply mkps_morphism; auto with Arith. unfold adjust_series; simpl. rewrite series_shift_0. do 2 rewrite series_stretch_const. rewrite series_mul_1_l. rewrite <- series_stretch_stretch. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul. rewrite Z2Nat.inj_mul; auto with Arith; simpl. rewrite <- stretch_shift_series_distr. rewrite <- series_stretch_const with (k := (dd * dd)%positive). rewrite <- series_stretch_add_distr. apply stretch_morph; [ reflexivity | ]. subst c₁ cb₃ pb₃ f₂. eapply nth_root_tail_const_plus_tail with (L₁ := L₂); try eassumption; reflexivity. apply Z.lt_le_incl; assumption. eapply multiplicity_pos; eassumption. eapply multiplicity_pos; eassumption. eapply multiplicity_pos; eassumption. intros j Hj. destruct j; [ assumption | simpl ]. apply le_S_n in Hj. rewrite Nat.le_0_r in Hj; subst j; simpl. erewrite <- nth_pol_n with (c := c₁) (f₁ := f₂); try eassumption; [ | reflexivity ]. rewrite <- Hfb₁; assumption. eapply multiplicity_pos; eassumption. eapply multiplicity_pos; eassumption. subst c m₁ q₀; eapply f₁_in_K_1_mq₀; try eassumption. intros n. pose proof (Hri 1%nat (Nat.le_refl 1)) as HH; simpl in HH. rewrite <- Hc, <- Hf₁, <- HL₁, <- Hc₁ in HH. rewrite HH. eapply le_trans; [ apply Hrle with (n := S n) | simpl ]. rewrite <- Hc, <- Hf₁, HL₁; apply Nat.le_refl. pose proof (Hri O Nat.le_0_1) as H₁; simpl in H₁. rewrite <- Hc in H₁; rewrite H₁. pose proof (Hreq O (Nat.le_0_l b₁)) as H₂; simpl in H₂. rewrite <- Hc₁ in H₂. symmetry; assumption. reflexivity. intros i Hib. destruct i; [ apply Hri, Nat.le_0_1 | simpl ]. rewrite <- Hc, <- Hf₁, <- HL₁. apply Hreq, Nat.succ_le_mono, Hib. 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