A proper plane section has total multiplicity at least N at no more than d*m/N distinct smooth points. The proof uses local expansions and polynomial interpolation.

theorem CCDN.formal_plane_multiplicity_bound {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (z : ι → Fin 2 → K) (hz : Function.Injective z) (ψ : ι → MvPolynomial (Fin 2) K →ₐ[K] PowerSeries K) (hψ : ∀ (i : ι), (ψ i) f = 0) (hconst : ∀ (i : ι) (h : MvPolynomial (Fin 2) K), PowerSeries.constantCoeff ((ψ i) h) = (MvPolynomial.eval (z i)) h) (j : ι → Fin 2) (hparam : ∀ (i : ι), (ψ i) (MvPolynomial.X (j i) - MvPolynomial.C (z i (j i))) = PowerSeries.X) (g : MvPolynomial (Fin 2) K) (hnd : ¬f ∣ g) (N : ℕ) (hvan : ∀ (i : ι), PowerSeries.X ^ N ∣ (ψ i) g) : Fintype.card ι * N ≤ f.totalDegree * g.totalDegree

Bézout with a uniform lower bound on vanishing at distinct formal branches.