let a, b be Nat; :: thesis: a + b divides (a |^ 2) - (b |^ 2)
(a |^ 2) - (b |^ 2) = (a + b) * (a - b) by Th1;
hence a + b divides (a |^ 2) - (b |^ 2) ; :: thesis: verum