proposition: Theorem root_tail_split_1st_any_r : ∀ f L c f₁ L₁ c₁ m q₀ 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₀) 0 f₁ L₁ = root_head 0 0 f₁ L₁ + ps_monom 1%K (γ_sum 0 0 f₁ L₁) * root_tail (m * q₀) 1 f₁ L₁)%ps.
proof: Proof. intros f L c f₁ L₁ c₁ m q₀ r. intros HL Hm Hq₀ Hc Hf₁ HL₁ Hc₁ Hri Hrle. remember (m * q₀)%positive as m₁. unfold root_tail, root_head; simpl. destruct (ps_zerop _ (ps_poly_nth 0 f₁)) as [H₁| H₁]. rewrite rng_add_0_l, rng_mul_0_r; reflexivity. assert (0 ≤ 1)%nat as H by apply Nat.le_0_l. apply Hri in H; simpl in H; rewrite <- Hc in H. rename H into Hr₀; move Hr₀ before Hc. assert (1 ≤ 1)%nat as H by apply Nat.le_refl. apply Hri in H; simpl in H; rewrite <- Hc, <- Hf₁, <- HL₁, <- Hc₁ in H. rename H into Hr₁; move Hr₁ before Hc₁. rename H₁ into Hnz₁. remember HL as HK₁; clear HeqHK₁. eapply next_pol_in_K_1_mq in HK₁; try eassumption . rewrite <- Heqm₁ in HK₁. remember HL as H; clear HeqH. eapply r_n_next_ns in H; try eassumption . destruct H as (αj₁, (αk₁, H)). destruct H as (Hini₁, (Hfin₁, (Hαj₁, Hαk₁))). remember HL as H; clear HeqH. eapply multiplicity_is_pos in H; try eassumption . rename H into Hrpos. remember Hrpos as H; clear HeqH. apply Nat2Z.inj_lt in H; simpl in H. rename H into Hrpos₁. remember Hrpos as H; clear HeqH. apply Nat.sub_gt in H. rewrite Nat.sub_0_r in H. rename H into Hrpos₃. remember HL as H; clear HeqH. eapply next_has_root_0_or_newton_segments in H; [ | eassumption | reflexivity ]. simpl in H; rewrite <- Hc, <- Hf₁ in H. destruct H as [| H]; [ contradiction | idtac ]. rename H into HL₁nz. remember HL₁ as HL₁₁; clear HeqHL₁₁. eapply hd_newton_segments in HL₁₁; try eassumption. remember HL₁₁ as HK₂; clear HeqHK₂. eapply next_pol_in_K_1_mq in HK₂; try eassumption; try reflexivity. remember HL₁₁ as H; clear HeqH. symmetry in Hr₁. eapply q_eq_1_any_r in H; try eassumption; [ idtac | reflexivity ]. rewrite H in HK₂; clear H. rewrite Pos.mul_1_r in HK₂. unfold γ_sum; simpl. unfold summation; simpl. do 2 rewrite rng_add_0_r. rewrite <- Hc₁. remember (next_pol f₁ (β L₁) (γ L₁) c₁) as f₂ eqn:Hf₂ . remember (option_get phony_ns (newton_segments f₂)) as L₂ eqn:HL₂ . destruct (ps_zerop _ (ps_poly_nth 0 f₂)) as [H₁| H₁]. rewrite ps_mul_0_r, ps_add_0_r. unfold root_tail_from_cγ_list, ps_monom; simpl. rewrite Hini₁, Hfin₁; simpl. rewrite Hαk₁; simpl. rewrite Qnum_inv_Qnat_sub; [ | assumption ]. rewrite Qden_inv_Qnat_sub; [ | assumption ]. rewrite Z.mul_1_r, Nat.sub_0_r. rewrite Z.add_0_r. rewrite Z.mul_shuffle0, Pos_mul_shuffle0. rewrite Pos2Z.inj_mul. rewrite Z.div_mul_cancel_r; try apply Pos2Z_ne_0. rewrite fold_series_const. symmetry in Hr₁. erewrite αj_m_eq_p_r; try eassumption; [ idtac | reflexivity ]. rewrite Pos2Z.inj_mul, Z.mul_shuffle0, Zposnat2Znat; [ | assumption ]. rewrite <- Z.mul_assoc. rewrite <- Zposnat2Znat; simpl; try eassumption . rewrite Z.div_mul; [ | apply Pos2Z_ne_0 ]. remember (Pos.of_nat r) as pr. remember (Qden αj₁ * pr * Qden αk₁)%positive as x. rewrite ps_adjust_eq with (n := O) (k := x); symmetry. rewrite ps_adjust_eq with (n := O) (k := m₁); symmetry. unfold adjust_ps; simpl. do 2 rewrite series_shift_0. rewrite series_stretch_const. do 2 rewrite Z.sub_0_r. rewrite Pos.mul_comm. apply mkps_morphism; [ | | reflexivity ]. symmetry. rewrite <- series_stretch_const with (k := x); subst x. apply stretch_morph; [ reflexivity | ]. constructor; intros i; simpl. unfold root_tail_series_from_cγ_list; simpl. rewrite <- Hc₁, <- Hf₂, <- HL₂. destruct (ps_zerop K (ps_poly_nth 0 f₁)); [ contradiction | ]. destruct i; [ reflexivity | simpl ]. destruct (ps_zerop K (ps_poly_nth 0 f₂)); [ | contradiction ]. reflexivity. subst x. rewrite Z.mul_shuffle0. rewrite Pos2Z.inj_mul, Z.mul_assoc. apply Z.mul_cancel_r; [ apply Pos2Z_ne_0 | ]. rewrite Pos.mul_comm, Pos2Z.inj_mul, Z.mul_assoc; symmetry. subst pr. rewrite Zposnat2Znat; [ | assumption ]. eapply αj_m_eq_p_r; try eassumption; reflexivity. rename H₁ into Hnz₂. pose proof (Hrle 2%nat) as H. remember (S 0) as one in H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H. subst one; simpl in H. rewrite <- Hc₁, <- Hf₂, <- HL₂ in H. rename H into Hrle₂. remember (ac_root (Φq f₂ L₂)) as c₂ eqn:Hc₂ . remember (root_multiplicity acf c₂ (Φq f₂ L₂)) as r₂ eqn:Hr₂ . symmetry in Hr₁, Hr₂. remember HL₁₁ as H; clear HeqH. eapply next_ns_r_non_decr in H; try eassumption . destruct H as (Heq, H); move Heq at top; subst r₂. clear Hrle₂; destruct H as (αj₂, (αk₂, H)). destruct H as (Hini₂, (Hfin₂, (Hαj₂, Hαk₂))). remember HL as H; clear HeqH. eapply next_ns_in_f in H; try eassumption . rename H into HL₁i; move HL₁i before HL₁. unfold root_tail_from_cγ_list; simpl. unfold ps_add, ps_mul; simpl. unfold cm; simpl. unfold ps_terms_add; simpl. unfold ps_ordnum_add; simpl. rewrite Hini₁, Hfin₁, Hini₂, Hfin₂; simpl. rewrite Hαk₁, Hαk₂; simpl. rewrite Qnum_inv_Qnat_sub; [ | assumption ]. rewrite Qden_inv_Qnat_sub; [ | assumption ]. rewrite Nat.sub_0_r. do 2 rewrite Z.add_0_r, Z.mul_1_r. remember (Pos.of_nat r) as rq eqn:Hrq . remember (Qnum αj₁ * Zpos (Qden αk₁))%Z as nd. remember (Qden αj₁ * Qden αk₁ * rq)%positive as dd. rewrite Z.mul_shuffle0, Pos_mul_shuffle0. do 3 rewrite Pos2Z.inj_mul. rewrite Z.div_mul_cancel_r; try apply Pos2Z_ne_0. rewrite Z.mul_add_distr_r. rewrite Z.mul_shuffle0, Z.mul_assoc; simpl. remember HL₁i as H; clear HeqH. eapply next_ns_in_f in H; try eassumption . rename H into HL₂i; move HL₂i before HL₂. remember (nd * Zpos dd * Zpos m₁)%Z as x. remember (Qnum αj₂ * Zpos m₁ / Zpos (Qden αj₂ * rq))%Z as y. rename Heqy into Hy. assert (x <= x + y * Zpos dd * Zpos dd)%Z as Hle. apply Z.le_sub_le_add_l. rewrite Z.sub_diag. subst y. apply Z.mul_nonneg_nonneg; [ | apply Pos2Z.is_nonneg ]. apply Z.mul_nonneg_nonneg; [ | apply Pos2Z.is_nonneg ]. destruct (Qnum αj₂); simpl. rewrite Z.div_0_l; [ reflexivity | apply Pos2Z_ne_0 ]. apply Z_div_pos_is_nonneg. apply Z.nle_gt in Hαj₂. exfalso; apply Hαj₂, Pos2Z.neg_is_nonpos. rewrite Z.min_l; [ | assumption ]. rewrite Z.min_r; [ | assumption ]. rewrite Z.sub_diag, Z.add_simpl_l; simpl. rewrite ps_adjust_eq with (n := O) (k := (dd * dd)%positive). unfold adjust_ps; simpl. rewrite series_shift_0. rewrite Z.sub_0_r. apply mkps_morphism. erewrite αj_m_eq_p_r in Hy; try eassumption; [ subst rq | reflexivity ]. rewrite <- Zposnat2Znat in Hy; [ simpl in Hy | assumption ]. rewrite Pos.mul_comm, Pos2Z.inj_mul in Hy. rewrite <- Z.mul_assoc in Hy; simpl in Hy. rewrite Z.div_mul in Hy; [ | apply Pos2Z_ne_0 ]. unfold adjust_series; simpl. rewrite series_shift_0. do 2 rewrite fold_series_const. do 2 rewrite series_stretch_const. rewrite series_mul_1_l. rewrite <- series_stretch_stretch. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul. remember Hini₂ as H; clear HeqH. eapply p_is_pos with (m := m₁) in H; try eassumption . rewrite <- Hy in H. rename H into Hppos. remember Hppos as H; clear HeqH. apply Z.lt_le_incl in H. rewrite Z2Nat.inj_mul; [ simpl | assumption | apply Pos2Z.is_nonneg ]. rewrite <- stretch_shift_series_distr. rewrite <- series_stretch_const with (k := (dd * dd)%positive). rewrite <- series_stretch_add_distr. apply stretch_morph; [ reflexivity | idtac ]. unfold series_add; simpl. constructor; intros i; simpl. destruct (lt_dec i (Z.to_nat y)) as [H₁| H₁]. destruct (zerop i) as [H₂| H₂]. subst i; simpl. rewrite rng_add_0_r. unfold root_tail_series_from_cγ_list; simpl. rewrite <- Hc₁. destruct (ps_zerop K (ps_poly_nth 0 f₁)); [ contradiction | ]. reflexivity. rewrite rng_add_0_l. unfold root_tail_series_from_cγ_list; simpl. rewrite <- Hc₁, <- Hf₂, <- HL₂. rewrite Hy in H₁. erewrite <- next_pow_eq_p in H₁; try eassumption . destruct i; [ exfalso; revert H₂; apply Nat.lt_irrefl | idtac ]. clear H₂; simpl. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [| H₂]; [ reflexivity | ]. clear H₂. destruct (ps_zerop K (ps_poly_nth 0 f₂)) as [| H₂]; [ reflexivity | ]. clear H₂. remember (next_pow 0 L₂ m₁) as p₂ eqn:Hp₂ . remember (Nat.compare p₂ (S i)) as cmp; symmetry in Heqcmp. destruct cmp; [ | | reflexivity ]. apply nat_compare_eq in Heqcmp. rewrite Heqcmp in H₁. exfalso; revert H₁; apply Nat.lt_irrefl. apply nat_compare_lt in Heqcmp. apply Nat.lt_le_incl, Nat.nlt_ge in Heqcmp. contradiction. apply Nat.nlt_ge in H₁. destruct (zerop i) as [H₂| H₂]. subst i; simpl. apply Nat.le_0_r in H₁. rewrite <- Z2Nat.inj_0 in H₁. apply Z2Nat.inj in H₁; [ | assumption | reflexivity ]. rewrite H₁ in Hppos. exfalso; revert Hppos; apply Z.lt_irrefl. rewrite rng_add_0_l. remember (Z.to_nat y) as n₂. remember (i - n₂)%nat as id. unfold root_tail_series_from_cγ_list. clear H. symmetry in Hr₁. remember HL₁i as H; clear HeqH. eapply q_eq_1_any_r in H; try eassumption; [ idtac | reflexivity ]. rename H into Hq₁; move Hq₁ before HL₁nz. symmetry in Hr₂. remember HL₂i as H; clear HeqH. eapply q_eq_1_any_r in H; try eassumption; [ idtac | reflexivity ]. rename H into Hq₂; move Hq₂ before Hnz₂. assert (∀ n, r ≤ nth_r n f₁ L₁) as Hrle₁. eapply all_r_le_next with (f := f); eassumption . move Hrle₁ before Hrle. assert (∀ n, r ≤ nth_r n f₂ L₂) as Hrle₂. eapply all_r_le_next with (f := f₁); eassumption . move Hrle₂ before Hrle₁. rewrite find_coeff_iter_succ with (r := r); try eassumption; [ symmetry | symmetry; assumption | apply Nat.lt_succ_diag_r ]. rewrite find_coeff_iter_succ with (r := r); try eassumption; [ symmetry | symmetry; assumption | apply Nat.lt_succ_diag_r ]. subst x; clear Hle. remember (S i) as si. remember (S (S id)) as x; simpl; subst x. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₄| H₄]. contradiction. destruct i; [ exfalso; revert H₂; apply Nat.lt_irrefl | idtac ]. rewrite <- Hc₁, <- Hf₂, <- HL₂; symmetry. rewrite <- find_coeff_add with (dp := n₂). rewrite Heqid. rewrite Nat.add_0_l, Nat.sub_add; [ | assumption ]. rewrite <- Heqid. subst si; remember (S i) as si. rewrite Hy in Heqn₂. symmetry in Hr₂. erewrite <- next_pow_eq_p in Heqn₂; try eassumption . remember (S id) as sid. subst n₂; simpl. destruct (ps_zerop K (ps_poly_nth 0 f₂)) as [H₃| H₃]. reflexivity. remember (next_pow 0 L₂ m₁) as pow₁ eqn:Hpow₁ . remember (Nat.compare pow₁ si) as cmp₁ eqn:Hcmp₁ . symmetry in Hcmp₁. destruct cmp₁; [ reflexivity | | reflexivity ]. rewrite <- Hc₂. remember (next_pol f₂ (β L₂) (γ L₂) c₂) as f₃. remember (option_get phony_ns (newton_segments f₃)) as L₃. destruct (ps_zerop _ (ps_poly_nth 0 f₃)) as [H₅| H₅]. subst si sid; simpl. destruct (ps_zerop _ (ps_poly_nth 0 f₃)) as [H₆| H₆]. reflexivity. contradiction. rename H₅ into Hnz₃. replace pow₁ with (0 + pow₁)%nat by reflexivity. rewrite next_pow_add. apply Nat.add_cancel_r with (p := pow₁) in Heqid. rewrite Nat.sub_add in Heqid; [ | assumption ]. rewrite <- Heqid. do 2 rewrite find_coeff_add. subst sid. remember HL₂i as H; clear HeqH. eapply next_ns_in_f in H; try eassumption . rename H into HL₃i. remember HL₂i as H; clear HeqH. symmetry in Hq₂. eapply next_pol_in_K_1_mq with (q := xH) in H; try eassumption . rewrite Pos.mul_1_r in H. rename H into HK₃. pose proof (Hrle₁ 2%nat) as H. remember (S 0) as one; simpl in H. rewrite <- Hc₁, <- Hf₂, <- HL₂ in H. subst one; simpl in H. rename Heqf₃ into Hf₃. rename HeqL₃ into HL₃. rewrite <- Hc₂, <- Hf₃, <- HL₃ in H. remember (ac_root (Φq f₃ L₃)) as c₃ eqn:Hc₃ . remember (root_multiplicity acf c₃ (Φq f₃ L₃)) as r₃ eqn:Hr₃ . rename H into Hrr. remember HL₂i as H; clear HeqH. symmetry in Hr₃. eapply next_ns_r_non_decr in H; try eassumption ; clear Hrr. destruct H as (Heq, H); move Heq at top; subst r₃. destruct H as (αj₃, (αk₃, H)). destruct H as (Hini₃, (Hfin₃, (Hαj₃, Hαk₃))). remember HL₃i as H; clear HeqH. symmetry in Hr₃. eapply q_eq_1_any_r in H; try eassumption; [ idtac | reflexivity ]. rename H into Hq₃. assert (∀ n, r ≤ nth_r n f₃ L₃) as Hrle₃. eapply all_r_le_next with (f := f₂); eassumption . move Hrle₃ before Hrle₂. symmetry in Hr₃. eapply find_coeff_more_iter; try eassumption; [ apply Nat.lt_succ_diag_r | ]. erewrite next_pow_eq_p in Hpow₁; try eassumption . rewrite <- Hy in Hpow₁. destruct pow₁. rewrite <- Z2Nat.inj_0 in Hpow₁. apply Z2Nat.inj in Hpow₁; [ idtac | reflexivity | idtac ]. rewrite <- Hpow₁ in Hppos. exfalso; revert Hppos; apply Z.lt_irrefl. apply Z.lt_le_incl; assumption. rewrite Nat.add_succ_r, <- Nat.add_succ_l. apply Nat.le_sub_le_add_l. rewrite Nat.sub_diag; apply Nat.le_0_l. subst x. rewrite Z.mul_shuffle0, Pos2Z.inj_mul, Z.mul_assoc. apply Z.mul_cancel_r; [ apply Pos2Z_ne_0 | ]. rewrite Z.mul_comm. rewrite <- Z.divide_div_mul_exact; [ | apply Pos2Z_ne_0 | ]. rewrite Z.mul_comm. apply Z.div_mul, Pos2Z_ne_0. rewrite Heqdd, Heqnd. rewrite Pos_mul_shuffle0, Z.mul_shuffle0, Pos2Z.inj_mul. apply Z.mul_divide_mono_r. erewrite αj_m_eq_p_r with (L₁ := L₁); try eassumption; try reflexivity. rewrite Pos.mul_comm, Hrq. rewrite Pos2Z.inj_mul, Zposnat2Znat; [ | assumption ]. exists (p_of_m m₁ (γ L₁)). rewrite Z.mul_assoc; reflexivity. rewrite Pos.mul_comm, Pos.mul_assoc; 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