let b, c be Nat; :: thesis: ( b,c are_coprime implies ((2 * b) + c) gcd c <= 2 )
assume A1: b,c are_coprime ; :: thesis: ((2 * b) + c) gcd c <= 2
A3: ((2 * b) + (c * 1)) gcd c = (2 * b) gcd c by EULER_1:8;

per cases ( c is odd or c is even ) ;

suppose c is odd ; :: thesis: ((2 * b) + c) gcd c <= 2

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

end;

suppose c is even ; :: thesis: ((2 * b) + c) gcd c <= 2

hence ((2 * b) + c) gcd c <= 2 by A1, A3, Lm5b; :: thesis: verum

end;

end;