theorem LemmaCong: :: NUMBER06:20

for n, k, l being Nat holds
( 3 divides n + l iff 3 divides (n + l) + (3 * k) )