for a, b being Integer holds a gcd b divides a by Def2;