understanding the Haskell implementation of the least divisor function
Ok, first LD(n) is the least divisor of n. It is a number, p, such
that p*a = n and a > p and p > 1.
So now to express LD(n) as a Haskell function:
ld n = ldf 2 n
Where ldf 2 n means the least divisor of n that is >= 2.
Hopefully it is understood that the Haskell expression of ld(n) is
equivalent to our initial mathematical definition.
Now, something else that is asserted and then proved:
n > 1 and n not prime IMPLIES (LD(n))^2 less than or equal to n
So then the following definition of ldf k n is offered
ld n = ldf 2 n ldf k n | divides n k = k | k^2 > n = n | otherwise = ldf (k+1) n
But I do not understand why the second guard is true. Clearly it has
to do with "n > 1 and n not prime IMPLIES (LD(n))^2 <= n" but I do not
see how they relate.