proposition: Theorem multiplicity_pos : ∀ f L r, (∀ i : nat, i ≤ 1 → nth_r i f L = r) → newton_segments f = Some L → (0 < r)%nat.
proof: Proof. intros f L r Hri HL. eapply multiplicity_is_pos; try eassumption; [ reflexivity | ]. pose proof (Hri O Nat.le_0_1) as H; simpl 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