let a, b be Integer; :: thesis: ( a >= 0 & b >= 0 implies a gcd b = a gcd (b - a) )
assume that
A1: a >= 0 and
A2: b >= 0 ; :: thesis: a gcd b = a gcd (b - a)
thus a gcd b = |.a.| gcd |.b.| by INT_2:34
.= |.a.| gcd |.(|.b.| - |.a.|).| by Th96
.= |.a.| gcd |.(b - |.a.|).| by A2, ABSVALUE:def 1
.= |.a.| gcd |.(b - a).| by A1, ABSVALUE:def 1
.= a gcd (b - a) by INT_2:34 ; :: thesis: verum