Description: A positive integer which divides both positive operands of the gcd operator is bounded by it. (Contributed by AV, 9-Aug-2020)