Description: Define the "k-regular" predicate, which is true for a "graph" being
k-regular: read G RegGraph K as " G is K-regular" or " G
is a K-regular graph". Note that K is allowed to be positive
infinity ( K e. NN0* ), as proposed by GL. (Contributed by Alexander
van der Vekens, 6-Jul-2018)(Revised by AV, 26-Dec-2020)