for a, b being Integer st b <> 0 holds
(a mod b) gcd b = a gcd b by Th8, WSIERP_1:43;