(n * (n - 1)) / 2 is Integer by Th2;
then (s * ((n / 2) * (n - 1))) + 1 is Integer ;
hence (((s * n) / 2) * (n - 1)) + 1 is Integer ; :: thesis: verum