mathlib

c65d8079 - feat(data/polynomial/erase_lead + data/polynomial/reverse): rename an old lemma, add a stronger one (#12909)

feat(data/polynomial/erase_lead + data/polynomial/reverse): rename an old lemma, add a stronger one (#12909) Taking advantage of nat-subtraction in edge cases, a lemma that previously proved `x ≤ y` actually holds with `x ≤ y - 1`. Thus, I renamed the old lemma to `original_name_aux` and `original_name` is now the name of the new lemma. Since this lemma was used in a different file, I used the `_aux` name in the other file. Note that the `_aux` lemma is currently an ingredient in the proof of the stronger lemma. It may be possible to have a simple direct proof of the stronger one that avoids using the `_aux` lemma, but I have not given this any thought.