let p be prime Nat; :: thesis: for k being non zero Nat st k < p holds
not p divides (p |^ 2) - (k |^ 2)
let k be non zero Nat; :: thesis: ( k < p implies not p divides (p |^ 2) - (k |^ 2) )
reconsider a = k - 1 as Nat ;
( p divides (p - (a + 1)) * (p + (a + 1)) implies a + 1 >= p ) by PSQ;
hence ( k < p implies not p divides (p |^ 2) - (k |^ 2) ) by NEWTON01:1; :: thesis: verum