Commit 2022-03-28 06:13 c65d8079

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.