2 divides a by ABIAN:def 1;
then consider k being Integer such that
A1: a = 2 * k ;
k,1 are_coprime ;
then (2 * k) gcd (2 * 1) = |.2.| by INT_2:24;
hence a gcd 2 = 2 by A1; :: thesis: verum