let m, n be Element of NAT ; :: thesis: m gcd n = m gcd (n + m)
set a = m gcd n;
set b = m gcd (n + m);
A1: m gcd n divides m by NAT_D:def 5;
A2: m gcd (n + m) divides m by NAT_D:def 5;
m gcd (n + m) divides n + m by NAT_D:def 5;
then m gcd (n + m) divides n by A2, NAT_D:10;
then A3: m gcd (n + m) divides m gcd n by A2, NAT_D:def 5;
m gcd n divides n by NAT_D:def 5;
then m gcd n divides n + m by A1, NAT_D:8;
then m gcd n divides m gcd (n + m) by A1, NAT_D:def 5;
hence m gcd n = m gcd (n + m) by A3, NAT_D:5; :: thesis: verum