mathlib

af3911c1 - feat(data/polynomial/erase_lead): add two erase_lead lemmas (#12910)

feat(data/polynomial/erase_lead): add two erase_lead lemmas (#12910) The two lemmas show that removing the leading term from the sum of two polynomials of unequal `nat_degree` is the same as removing the leading term of the one of larger `nat_degree` and adding. The second lemma could be proved with `by rw [add_comm, erase_lead_add_of_nat_degree_lt_left pq, add_comm]`, but I preferred copying the same strategy as the previous one, to avoid interdependencies.