for p being prime Nat
for a, b being Nat st a <> b holds
p |-count (a + b) >= p |-count (a gcd b)