proposition: Theorem upper_bound_zerop_1st_when_r_constant : ∀ f L c f₁ L₁ m q₀ r ofs, newton_segments f = Some L → c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → (ps_poly_nth 0 f ≠ 0)%ps → m = ps_pol_com_polydo f → q₀ = q_of_m m (γ L) → root_multiplicity acf c (Φq f L) = S r → (∀ i : nat, if multiplicity_decreases f L i then False else True) → (order (ps_pol_apply f₁ (root_tail (m * q₀) 0 f₁ L₁)) = qfin ofs)%Qbar → ∀ N, N = Z.to_nat (2 * Zpos m * Zpos q₀ * Qnum ofs) → zerop_1st_n_const_coeff N f₁ L₁ = true.
proof: Proof. intros f L c f₁ L₁ m q₀ r ofs. intros HL Hc Hf₁ HL₁ Hnz₀ Hm Hq₀ Hr Hn Hofs N HN. apply not_false_iff_true; intros Hz. assert (Hrle : ∀ n : nat, S r ≤ nth_r n f L). rewrite Hc in Hr. apply multiplicity_not_decreasing; assumption. remember (1 # 2 * m * q₀) as η eqn:Hη . assert (Hηβ : ∀ i, i ≤ N → η < β (nth_ns i f₁ L₁)). intros i Hi. clear HN. revert HL Hc Hf₁ HL₁ Hnz₀ Hm Hq₀ Hr Hrle Hη N Hi Hz; clear; intros. subst c q₀. eapply β_lower_bound_r_const with (n := i) (r := S r); try eassumption. pose proof (exists_pol_ord K f) as H. destruct H as (m', (Hm', Hp)). rewrite <- Hm in Hm'; subst m'. apply Hp. apply Nat.lt_0_succ. eapply zerop_1st_n_const_coeff_false_before; eassumption. apply non_decr_imp_eq; try assumption. apply zerop_1st_n_const_coeff_false_succ; [ assumption | simpl ]. rewrite <- Hf₁, <- HL₁. eapply zerop_1st_n_const_coeff_false_before; eassumption. apply eq_refl. remember (@summation _ Q_ring O N (λ i, β (nth_ns i f₁ L₁))) as u eqn:Hu . assert (Huo : u <= ofs). rewrite Hc in Hf₁. revert HL Hc Hf₁ HL₁ Hnz₀ Hm Hq₀ Hr Hofs Hz Hrle Hu; clear; intros. rewrite root_tail_when_r_r with (n := N) (r := (S r)) in Hofs; try eassumption. rewrite apply_nth_pol in Hofs; [ | assumption ]. rewrite <- Hu in Hofs. destruct (fld_zerop 1%K) as [H₀| H₀]. rewrite H₀ in Hofs. rewrite ps_zero_monom_eq in Hofs. rewrite ps_mul_0_l in Hofs. rewrite order_0 in Hofs. symmetry in Hofs. apply eq_Qbar_qinf in Hofs. discriminate Hofs. rewrite order_mul in Hofs. rewrite ps_monom_order in Hofs; [ | assumption ]. apply Qbar.qfin_le_mono. rewrite <- Hofs. apply Qbar.le_sub_le_add_l. rewrite Qbar.sub_diag. apply order_pol_apply_nonneg. intros a Ha. remember (nth_pol N f₁ L₁) as polN eqn:HpolN . remember (nth_ns N f₁ L₁) as LN eqn:HLN . assert (H : newton_segments polN = Some LN). eapply in_newton_segment_when_r_constant; eassumption. eapply f₁_orders in H; try eassumption; try apply eq_refl. erewrite <- nth_pol_succ in H; try eassumption. destruct H as (H, _). apply List_In_nth with (d := 0%ps) in Ha. destruct Ha as (n, Hn₁). rewrite Hn₁. apply H. symmetry. apply nth_c_n; try eassumption. rewrite Nat.add_0_l. rewrite <- Hc in Hf₁. eapply order_root_tail_nonneg_any_r; try eassumption. rewrite zerop_1st_n_const_coeff_succ; simpl. rewrite <- Hc, <- Hf₁, <- HL₁, Hz. remember (ps_poly_nth 0 f) as x. destruct (ps_zerop K x); [ contradiction | reflexivity ]. pose proof (exists_pol_ord K f) as H. destruct H as (m', (Hm', Hp)). rewrite <- Hm in Hm'; subst m'. apply Hp. apply non_decr_imp_eq; auto with Arith. apply zerop_1st_n_const_coeff_false_iff. intros j Hj. destruct j; [ assumption | ]. apply le_S_n in Hj. apply Nat.le_0_r in Hj; subst j; simpl. rewrite <- Hf₁. rewrite zerop_1st_n_const_coeff_false_iff in Hz. pose proof (Hz O (Nat.le_0_l N)) as H₁. assumption. simpl; rewrite <- Hc; assumption. rewrite zerop_1st_n_const_coeff_succ; simpl. rewrite <- Hf₁, <- HL₁, Hz. remember (ps_poly_nth 0 f) as x. destruct (ps_zerop K x); [ contradiction | reflexivity ]. assert (Hou : ofs < u). clear Hofs Hn. subst u. apply summation_all_lt in Hηβ. eapply Qle_lt_trans; try eassumption. rewrite Hη, HN. rewrite <- Pos2Z.inj_mul. rewrite <- Pos2Z.inj_mul. remember (2 * m * q₀)%positive as mq eqn:Hmq . rewrite Z.mul_comm. rewrite Z2Nat_inj_mul_pos_r. unfold Qle; simpl. rewrite Pos.mul_1_r. rewrite Pos2Z.inj_mul. rewrite Zpos_P_of_succ_nat. rewrite Nat2Z.inj_mul. remember (Qnum ofs) as nofs eqn:Hnofs . symmetry in Hnofs. destruct nofs as [| nofs| nofs]; simpl; auto with Arith. rewrite positive_nat_Z. rewrite Z.mul_succ_l. rewrite positive_nat_Z. rewrite <- Pos2Z.inj_mul. rewrite <- Z.mul_1_r at 1. eapply Z.le_trans. apply Z.mul_le_mono_nonneg_l with (m := (Zpos (Qden ofs))%Z); auto with Arith. rewrite Z.one_succ. apply Zlt_le_succ. apply Pos2Z.is_pos. apply Z.le_sub_le_add_l. rewrite Z.sub_diag; apply Pos2Z.is_nonneg. apply Zle_neg_pos. apply Qlt_not_le in Hou; contradiction . 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