proposition: Theorem all_r_le_next : ∀ f L c f₁ L₁ r, c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → (∀ n : nat, r ≤ nth_r n f L) → (∀ n : nat, r ≤ nth_r n f₁ L₁).
proof: Proof. intros f L c f₁ L₁ r Hc Hf₁ HL₁ Hri i. pose proof (Hri (S i)) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H. 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