let a be Nat; :: thesis: a,(2 * a) + 1 are_coprime
assume not a,(2 * a) + 1 are_coprime ; :: thesis: contradiction
then consider n being Nat such that
A1: ( n divides a & n divides (2 * a) + 1 & n <> 1 ) by PYTHTRIP:def 1;
A2: 1 divides n by NAT_D:6;
n divides 2 * a by A1, NAT_D:9;
then n divides 1 by A1, NAT_D:10;
hence contradiction by A1, A2, NAT_D:5; :: thesis: verum