for b, c being Nat st (b + c) gcd b = 1 & c is odd holds
((2 * b) + c) gcd c = 1