Commit 2021-12-12 15:54 61b0f419

refactor(data/{mv_,}polynomial): lemmas about adjoin (#10670) Prove adjoin {X} = ⊤ and adjoin (range X) = ⊤ for polynomials and mv_polynomials much earlier and use these equalities to golf some proofs. Also drop some comm_ in typeclass assumptions.