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