Correctness of the sparse trinomial coefficient generator

Each of the three distinguished positions lies inside the output list. For a positive half-degree they are distinct; at zero, all three unit coefficients sum to one in ZMod 2.

theorem Complexity.BitPolynomial.Internal.trinomialBits_length (d : ℕ) : (trinomialBits d).length = 2 * d + 1

theorem Complexity.BitPolynomial.Internal.ofBits_trinomialBits (d : ℕ) : ofBits (trinomialBits d) = Polynomial.X ^ (2 * d) + Polynomial.X ^ d + 1