Is it right for this theory to base itself on HOL.Deriv rather than Complex_Main? Larry section ‹Polynomials as type over a ring structure› theory Polynomial imports HOL.Deriv "HOL-Library.More_List" "HOL-Library.Infinite_Set" Factorial_Ring begin