proposition: Theorem order_root_tail_nonneg_any_r_aux : ∀ f L c f₁ L₁ 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 → (ps_poly_nth 0 (nth_pol i f L) ≠ 0)%ps) → (∀ i, i ≤ S n → nth_r i f L = r) → (0 ≤ order (root_tail (m * q₀) n f₁ L₁))%Qbar.
proof: Proof. intros f L c f₁ L₁ m q₀ n r HL Hm Hq₀ Hc Hf₁ HL₁ Hpsi Hri. unfold root_tail. remember (zerop_1st_n_const_coeff n f₁ L₁) as z₁ eqn:Hz₁ . symmetry in Hz₁. destruct z₁; [ rewrite order_0; constructor | idtac ]. revert m q₀ c f L f₁ L₁ HL Hc Hm Hq₀ Hf₁ HL₁ Hz₁ Hpsi Hri. induction n; intros. simpl. unfold order; simpl. pose proof (Hpsi 1%nat (Nat.le_refl 1)) as H; simpl in H. rewrite <- Hc, <- Hf₁ in H. rename H into Hnz₁; move Hnz₁ before HL₁. pose proof (Hri 0%nat Nat.le_0_1) as H. simpl in H; rewrite <- Hc in H. rename H into Hr₀; move Hr₀ before Hc. pose proof (Hri 1%nat (Nat.le_refl 1)) as H. simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . move Hc₁ before HL₁. move c₁ before L₁. rename H into Hr₁; move Hr₁ before Hc₁. remember Hc as H; clear HeqH. eapply multiplicity_is_pos in H; try eassumption . rename H into Hrpos; move Hrpos before Hnz₁. remember HL₁ as H; clear HeqH. eapply r_n_next_ns in H; try eassumption . move H before Hnz₁. destruct H as (αj₁, (αk₁, H)). destruct H as (Hini₁, (Hfin₁, (Hαj₁, Hαk₁))). remember HL₁ as H; clear HeqH. eapply hd_newton_segments in H; try eassumption . rename H into HL₁i; move HL₁i before HL₁. remember HL as H; clear HeqH. eapply next_pol_in_K_1_mq in H; try eassumption . remember (m * q₀)%positive as m₁ eqn:Hm₁. rename H into HK₁; move HK₁ before Hnz₁. move Hm₁ before Hq₀. rewrite Hini₁, Hfin₁; simpl. rewrite Hαk₁; simpl. rewrite Qnum_inv_Qnat_sub; [ | apply Hrpos ]. rewrite Qden_inv_Qnat_sub; [ | apply Hrpos ]. rewrite Z.add_0_r, Z.mul_1_r. remember (root_tail_series_from_cγ_list m₁ f₁ L₁) as t. remember (series_order {| terms := t |} 0) as v eqn:Hv . symmetry in Hv. destruct v; [ idtac | constructor ]. apply Qbar.qfin_le_mono. rewrite Nat.sub_0_r. rewrite Z.mul_shuffle0, Pos_mul_shuffle0. rewrite Pos2Z.inj_mul. rewrite Z.div_mul_cancel_r; [ | apply Pos2Z_ne_0 | apply Pos2Z_ne_0 ]. erewrite αj_m_eq_p_r with (L₁ := L₁); try eassumption; [ | reflexivity ]. rewrite Z.mul_shuffle0. rewrite <- Zposnat2Znat; [ | assumption ]. rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul. rewrite Z.div_mul; [ | apply Pos2Z_ne_0 ]. unfold Qle; simpl. rewrite Z.mul_1_r. apply Z.add_nonneg_nonneg; [ idtac | apply Nat2Z.is_nonneg ]. apply Z.lt_le_incl. eapply p_is_pos; eassumption . simpl in Hz₁; simpl. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . remember (next_pol f₁ (β L₁) (γ L₁) c₁) as f₂ eqn:Hpol₂ . remember (option_get phony_ns (newton_segments f₂)) as L₂ eqn:HL₂ . destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₁| H₁]. discriminate Hz₁. remember (m * q₀)%positive as m₁ eqn:Hm₁ . replace m₁ with (m₁ * 1)%positive by apply Pos.mul_1_r. pose proof (Hri 0%nat (Nat.le_0_l (S (S n)))) as H. simpl in H; rewrite <- Hc in H. rename H into Hr₀; move Hr₀ before Hc. assert (1 ≤ S (S n)) as H by apply le_n_S, Nat.le_0_l. apply Hri in H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁, <- Hc₁ in H. rename H into Hr₁; move Hr₁ before Hc₁. remember Hc as H; clear HeqH. eapply multiplicity_is_pos in H; try eassumption . rename H into Hrpos; move Hrpos before HL₁. 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 hd_newton_segments in H; try eassumption . rename H into HL₁i; move HL₁i before HL₁. remember HL as H; clear HeqH. eapply next_pol_in_K_1_mq in H; try eassumption . rewrite <- Hm₁ in H. rename H into HK₁; move HK₁ before HL₁i. eapply IHn with (L := L₁) (f := f₁); try eassumption . symmetry in Hr₁; symmetry. eapply q_eq_1_any_r with (f := f₁); try eassumption; reflexivity. intros i Hin. apply Nat.succ_le_mono in Hin. apply Hpsi in Hin; simpl in Hin. rewrite <- Hc, <- Hf₁, <- HL₁ in Hin. assumption. intros i Hin. apply Nat.succ_le_mono in Hin. apply Hri in Hin; simpl in Hin. rewrite <- Hc, <- Hf₁, <- HL₁ in Hin. assumption. 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 RootAnyR