let b, c be Nat; :: thesis: ( (b + c) gcd b = 1 & c is odd implies ((2 * b) + c) gcd c = 1 )

assume A1: ( (b + c) gcd b = 1 & c is odd ) ; :: thesis: ((2 * b) + c) gcd c = 1

then (c + (b * 1)) gcd b = 1 ;

then A2: c gcd b = 1 by EULER_1:8;

((2 * b) + (c * 1)) gcd c = (2 * b) gcd c by EULER_1:8;

hence ((2 * b) + c) gcd c = 1 by A1, A2, Lm5a; :: thesis: verum

assume A1: ( (b + c) gcd b = 1 & c is odd ) ; :: thesis: ((2 * b) + c) gcd c = 1

then (c + (b * 1)) gcd b = 1 ;

then A2: c gcd b = 1 by EULER_1:8;

((2 * b) + (c * 1)) gcd c = (2 * b) gcd c by EULER_1:8;

hence ((2 * b) + c) gcd c = 1 by A1, A2, Lm5a; :: thesis: verum