HOL-ex.Cubic_Quartic