let a be natural number ; :: thesis: for b being integer number st a divides b holds
a gcd b = a
let b be integer number ; :: 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