theorem PMG: :: NEWTON05:78

for a being odd Nat
for b being non trivial odd Nat holds
( Parity (a + b) = min ((Parity (a + 1)),(Parity (b - 1))) or Parity (a + b) >= 2 * (Parity (a + 1)) )