proposition: Theorem q_eq_1_r_non_decr : ∀ f L c f₁ L₁ m r, newton_segments f = Some L → pol_in_K_1_m f m → q_of_m m (γ L) = 1%positive → 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 → root_multiplicity acf c (Φq f L) = r → (∀ i, r ≤ nth_r i f L) → q_of_m m (γ L₁) = 1%positive.
proof: Proof. intros f L c f₁ L₁ m r HL HK Hq Hc Hf₁ HL₁ Hnz₁ Hr₀ Hrle. remember HL as H; clear HeqH. eapply next_ns_in_f in H; try eassumption . rename H into HL₁i. pose proof (Hrle 1%nat) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . rename H into Hrle₁. remember (root_multiplicity acf c₁ (Φq f₁ L₁)) as r₁ eqn:Hr₁ . remember HL as H; clear HeqH. symmetry in Hr₁. eapply next_ns_r_non_decr in H; try eassumption . clear Hrle₁. 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 with (L := L₁); try eassumption; [ | reflexivity ]. replace m with (m * 1)%positive by apply Pos.mul_1_r. symmetry in Hq. eapply next_pol_in_K_1_mq with (L := L); eassumption. 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