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;

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;