take p = <%(0. R),(0. R),(1. R)%>; :: thesis: ( p is monic & p is purely_quadratic )
thus ( p is monic & p is purely_quadratic ) ; :: thesis: verum