let m, n be Nat; :: thesis: ( 0 < m implies m gcd n <= m )
m gcd n divides m by INT_2:def 2;
hence ( 0 < m implies m gcd n <= m ) by INT_2:27; :: thesis: verum