for a, b being Nat holds
( 163 divides a + b iff 163 divides (a |^ 163) + (b |^ 163) ) by NAT_4:35, Th60;