theory More_More_MPoly_Type imports Type_Casting Substitutions Poly_Expansions Total_Degree Variables Degree Notation begin end