Correctness of padded binary-polynomial addition

Each in-range XOR is addition in ZMod 2. Beyond the maximum operand length, all three coefficient lists represent zero coefficients.

theorem Complexity.BitPolynomial.Internal.addBits_length (a b : List Bool) : (addBits a b).length = max a.length b.length

theorem Complexity.BitPolynomial.Internal.ofBits_addBits (a b : List Bool) : ofBits (addBits a b) = ofBits a + ofBits b