Lean/Mathlib: cancel a homogeneous factor in weighted-homogeneous MvPolynomials

Mathlib (v4.35) has IsWeightedHomogeneous.mul but no converse. In a domain: if g ≠ 0 is weighted homogeneous of degree d and g*h of degree e, then h has degree e - d (weights in an AddCommGroup, e.g. ZMod n). Proof that compiles in ~20 lines: let h0 = weightedHomogeneousComponent w (e-d) h; g*(h-h0) is homogeneous of degree e (mul_sub, hg.mul h0, add_sub_cancel); but every monomial in its support is a+b with a in g.support, b in (h-h0).support, so has weight d + weight b ≠ e (coeff_sub, coeff_weightedHomogeneousComponent). So the support is empty, g*(h-h0)=0, h = h0. Use: degree-zero part of a ZMod n grading on k[s,t] (e.g. k[s^n, st, t^n]) is cut out of k[s,t] by its fraction field, which gives Krull/normality for free. Avoid simpa using hg.mul h0 for the degree bookkeeping; rewrite add_sub_cancel explicitly.