Least divisor function

Function

 definiendum $\mathrm{ld}:\mathbb N^+\to\{1\}\cup\mathrm{Prime\ number}$ definiendum $\mathrm{ld}(n):=\mathrm{min}\left(\mathrm{divisors}(n)\right)$

Code

divides :: Integral a => a -> a -> Bool
divides d n = rem n d == 0
ld :: Integral a => a -> a
ld n = ldf 2 n

ldf :: Integral a => a -> a -> a
ldf k n | divides k n = k
| k^2 > n     = n
| otherwise   = ldf (k+1) n

using Set of divisors function:

divides :: Integral a => a -> a -> Bool
divides d n = rem n d == 0

Theorems

If $n$ isn't a prime, then $n$ divided by the least divisor is some number bigger than $\mathrm{ld}(n)$ and hence

$\mathrm{ld}(n)^2\le n$