for a being Nat holds
( 7 divides (a |^ 7) + 1 iff 7 divides a + 1 ) by Th63, NAT_4:26;