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

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