let a be Nat; :: thesis: for b being Integer st a divides b holds
a gcd b = a
let b be Integer; :: thesis: ( a divides b implies a gcd b = a )
assume A1: a divides b ; :: thesis: a gcd b = a
for m being Integer st m divides a & m divides b holds
m divides a ;
hence a gcd b = a by A1, INT_2:def 2; :: thesis: verum