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 by NAT_D:def 5;
A2: m gcd n divides n by NAT_D:def 5;
A3: 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;
A4: abs (n - m) = nm by ABSVALUE:def 1;
then m gcd (abs (n - m)) divides nm by NAT_D:def 5;
then m gcd (abs (n - m)) divides nm + m by A3, NAT_D:8;
then A5: m gcd (abs (n - m)) divides m gcd n by A3, NAT_D:def 5;
m gcd n divides n - m by A1, A2, Th108;
then m gcd n divides m gcd (abs (n - m)) by A1, A4, NAT_D:def 5;
hence m gcd n = m gcd (abs (n - m)) by A5, NAT_D:5; :: thesis: verum

end;

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

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

end;

end;