let a, b be Nat; :: thesis: for u being Integer holds (a + (u * b)) gcd b = a gcd b
let u be Integer; :: thesis: (a + (u * b)) gcd b = a gcd b
b divides u * b ;
then A0: b gcd (u * b) = |.b.| by Th3
.= b ;

per cases ( a <> 0 or a = 0 ) ;

suppose a <> 0 ; :: thesis: (a + (u * b)) gcd b = a gcd b

hence (a + (u * b)) gcd b = a gcd b by EULER_1:16; :: thesis: verum

end;

suppose a = 0 ; :: thesis: (a + (u * b)) gcd b = a gcd b

hence (a + (u * b)) gcd b = a gcd b by A0; :: thesis: verum

end;

end;