let m, n be Element of NAT ; :: thesis: m gcd n = m gcd (abs (n - m))
set x = m gcd n;
set y = m gcd (abs (n - m));
A1: ( m gcd n divides m & m gcd n divides n ) by NAT_D:def 5;
A2: m gcd (abs (n - m)) divides m by NAT_D:def 5;

per cases ( n - m >= 0 or n - m < 0 ) ;

suppose n - m >= 0 ; :: thesis: m gcd n = m gcd (abs (n - m))

then reconsider nm = n - m as Element of NAT by INT_1:16;
A3: abs (n - m) = nm by ABSVALUE:def 1;
m gcd n divides n - m by A1, Th108;
then A4: m gcd n divides m gcd (abs (n - m)) by A1, A3, NAT_D:def 5;
m gcd (abs (n - m)) divides nm by A3, NAT_D:def 5;
then m gcd (abs (n - m)) divides nm + m by A2, NAT_D:8;
then m gcd (abs (n - m)) divides m gcd n by A2, NAT_D:def 5;
hence m gcd n = m gcd (abs (n - m)) by A4, NAT_D:5; :: thesis: verum

end;

suppose n - m < 0 ; :: thesis: m gcd n = m gcd (abs (n - m))

then A5: abs (n - m) = - (n - m) by ABSVALUE:def 1
.= m - n ;
then reconsider mn = m - n as Element of NAT ;
m gcd n divides m - n by A1, Th108;
then A6: m gcd n divides m gcd (abs (n - m)) by A1, A5, NAT_D:def 5;
m gcd (abs (n - m)) divides mn by A5, NAT_D:def 5;
then A7: m gcd (abs (n - m)) divides mn - m by A2, Th108;
reconsider nn = n as Integer ;
m gcd (abs (n - m)) divides nn by A7, INT_2:14;
then m gcd (abs (n - m)) divides m gcd n by A2, NAT_D:def 5;
hence m gcd n = m gcd (abs (n - m)) by A6, NAT_D:5; :: thesis: verum

end;

end;