Commit 2021-08-06 09:28 da32780c

chore(data/polynomial/*): create file data/polynomial/inductions and move around lemmas (#8563) This PR is a precursor to #8463: it performs the move, without introducing lemmas and squeezes some simps to make some proofs faster. I added add a doc-string to lemma degree_pos_induction_on with a reference to a lemma that will appear in #8463. The main reason why there are more added lines than removed ones is that the creation of a new file has a copyright statement, a module documentation and a few variable declarations.