((1 * a) + 1) gcd a = 1 gcd a by NEWTON02:5;
hence (a + 1) gcd a = 1 ; :: thesis: verum