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