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