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 ;
then A5: m gcd |.(n - m).| divides m gcd n by ;
m gcd n divides n - m by A1, A2, Th94;
then m gcd n divides m gcd |.(n - m).| by ;
hence m gcd n = m gcd |.(n - m).| by ; :: 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
.= m - n ;
then reconsider mn = m - n as Element of NAT ;
m gcd |.(n - m).| divides mn by ;
then m gcd |.(n - m).| divides mn - m by ;
then m gcd |.(n - m).| divides nn by INT_2:10;
then A8: m gcd |.(n - m).| divides m gcd n by ;
m gcd n divides m - n by A1, A2, Th94;
then m gcd n divides m gcd |.(n - m).| by ;
hence m gcd n = m gcd |.(n - m).| by ; :: thesis: verum
end;
end;