let a, b be Integer; :: thesis: ( a >= 0 & b >= 0 implies a gcd b = a gcd (b - a) )
assume A1: ( a >= 0 & b >= 0 ) ; :: thesis: a gcd b = a gcd (b - a)
thus a gcd b = (abs a) gcd (abs b) by INT_2:51
.= (abs a) gcd (abs ((abs b) - (abs a))) by Th110
.= (abs a) gcd (abs (b - (abs a))) by A1, ABSVALUE:def 1
.= (abs a) gcd (abs (b - a)) by A1, ABSVALUE:def 1
.= a gcd (b - a) by INT_2:51 ; :: thesis: verum