mathlib3

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