theorem Th10: :: BINARI_4:10

for n being non zero Nat
for l, m being Nat st l + m <= (2 to_power n) - 1 holds
add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE