mathlib

42df1860 - feat(data/polynomial/degree): `(n : ℕ) < p.degree ↔ n < p.nat_degree`