let m, n be Nat; :: thesis: m gcd n = m gcd |.(n - m).|
set x = m gcd n;
set y = m gcd |.(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 |.(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 |.(n - m).|

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

end;

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

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

end;

end;