Correctness of carryless polynomial multiplication

The product coefficient is a convolution over the two coefficient lists. Counting the true summands and reducing that count modulo two gives exactly mulBits, including its high zero padding and empty input cases.

theorem Complexity.BitPolynomial.Internal.ofBits_coeff (bits : List Bool) (k : ℕ) : (ofBits bits).coeff k = ↑(bits[k]?.getD false).toNat

theorem Complexity.BitPolynomial.Internal.mulBits_length (a b : List Bool) : (mulBits a b).length = a.length + b.length

theorem Complexity.BitPolynomial.Internal.ofBits_mulBits (a b : List Bool) : ofBits (mulBits a b) = ofBits a * ofBits b