take rpoly (1,(1. R)) ; :: thesis: ( not rpoly (1,(1. R)) is constant & rpoly (1,(1. R)) is monic )
thus ( not rpoly (1,(1. R)) is constant & rpoly (1,(1. R)) is monic ) ; :: thesis: verum