theorem Th9: :: NUMBER10:9

for m, n being Nat st m <= n holds
<=6n+1 m c= <=6n+1 n