for j, k being Nat st j <> 0 holds
j divides (j + k) !