proposition: Theorem multiplicity_is_pos : ∀ f L c r, newton_segments f = Some L → c = ac_root (Φq f L) → root_multiplicity acf c (Φq f L) = r → (0 < r)%nat.
proof: Proof. intros f L c r HL Hc Hr. remember HL as H; clear HeqH. eapply multiplicity_neq_0 in H; [ | eassumption ]. apply Nat.neq_sym, neq_0_lt in H. rewrite Hr 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