a gcd (a gcd b) = (a gcd a) gcd b by INT_6:18
.= (|.a.| gcd |.a.|) gcd b by INT_2:34 ;
hence a gcd (a gcd b) = a gcd b by INT_6:14; :: thesis: verum