proposition: Theorem β_lower_bound_r_const : ∀ f L f₁ L₁ m r η, newton_segments f = Some L → pol_in_K_1_m f m → (0 < r)%nat → f₁ = next_pol f (β L) (γ L) (ac_root (Φq f L)) → L₁ = option_get phony_ns (newton_segments f₁) → (∀ i, r ≤ nth_r i f L) → η = 1 # (2 * m * q_of_m m (γ L)) → ∀ n Ln, zerop_1st_n_const_coeff n f₁ L₁ = false → (∀ i, i ≤ S n → nth_r i f L = r) → Ln = nth_ns n f₁ L₁ → η < β Ln.
proof: Proof. intros f L f₁ L₁ m r η. intros HL Hm Hr Hf₁ HL₁ Hrle Hη n Ln Hnz Hri HLn. remember HL as H; clear HeqH. rewrite zerop_1st_n_const_coeff_false_iff in Hnz. eapply r_n_nth_ns in H; try eassumption; eauto with Arith. destruct H as (αjn, (αkn, H)). destruct H as (Hinin, (Hfinn, (Hαjn, Hαkn))). unfold β. rewrite Hinin; simpl. unfold Qnat; simpl. rewrite rng_mul_0_l, rng_add_0_r. remember Hf₁ as H; clear HeqH. eapply next_pol_in_K_1_mq in H; try eassumption; eauto with Arith. rename H into HK₁. pose proof (Hnz O (Nat.le_0_l n)) as Hnz₀. simpl in Hnz₀. assert (0 ≤ S n)%nat as H by apply Nat.le_0_l. apply Hri in H; simpl in H. rename H into Hr₀. assert (1 ≤ S n)%nat as H by apply le_n_S, Nat.le_0_l. apply Hri in H; simpl in H. rewrite <- Hf₁, <- HL₁ in H. rename H into Hr₁. remember HL₁ as H; clear HeqH. eapply r_n_next_ns in H; try eassumption; auto with Arith. 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. remember HK₁ as H; clear HeqH. eapply first_n_pol_in_K_1_m_any_r with (L := L₁) in H; eauto with Arith. rename H into HKn. remember (nth_pol n f₁ L₁) as fn eqn:Hfn . remember HL₁i as H; clear HeqH. eapply nth_in_newton_segments_any_r with (n := n) in H; eauto with Arith. rename H into HLni. remember HKn as H; clear HeqH. eapply pol_ord_of_ini_pt in H; try eassumption; eauto with Arith. rewrite Hη, H. rewrite <- Pos.mul_assoc. remember (m * q_of_m m (γ L))%positive as m₁ eqn:Hm₁ . unfold mh_of_m. erewrite <- qden_αj_is_ps_polydo; try eassumption; eauto with Arith. remember (2 * m₁)%positive as m₂. unfold Qlt; simpl; subst m₂. clear H. assert (0 < Qnum αjn * Zpos m₁ / Zpos (Qden αjn))%Z as H. apply Z2Nat.inj_lt; [ reflexivity | idtac | idtac ]. apply Z.div_pos; [ idtac | apply Pos2Z.is_pos ]. apply Z.mul_nonneg_nonneg; auto with Arith. apply Z.lt_le_incl; assumption. eapply num_m_den_is_pos with (L := Ln); try eassumption. rewrite Pos2Z.inj_mul, Z.mul_assoc. replace (Zpos m₁)%Z with (1 * Zpos m₁)%Z at 1 by reflexivity. apply Z.mul_lt_mono_pos_r; [ apply Pos2Z.is_pos | idtac ]. rewrite Z.mul_comm. apply Z.lt_1_mul_pos; auto with Arith. apply Z.lt_1_2. eapply q_eq_1_any_r with (L := L₁); try eassumption; eauto with Arith. intros i. rewrite HL₁, Hf₁. erewrite <- nth_pol_succ with (n := O); try eassumption; try reflexivity. erewrite <- nth_ns_succ with (n := O); try eassumption; try reflexivity. rewrite <- nth_r_add. apply Hrle. 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