Description: Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read G RegUSGraph K as G is a K-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 18-Dec-2020)