let m be Nat; :: thesis: m gcd 1 = 1
set M = m gcd 1;
A1: 1 divides m gcd 1 by NAT_D:6;
m gcd 1 divides 1 by NAT_D:def 5;
hence m gcd 1 = 1 by A1, NAT_D:5; :: thesis: verum