 A natural number \(y\) is said to be divisible by \(x\) just in case there exists a \(z\) such that \(x \times z = y\)—i.e., \(x\) divides \(y\) without remainder. In this case we write \(x \divides y\). Note that if \(x \divides y\) holds, then this must be witnessed by a divisor \(z \leq y\) such that \(x \times z = y\). We may thus define \(x \divides y\) in the following manner which shows that it is primitive recursive: 