Significant lengths of binary coefficient lists

The bounded maximum defining significant length identifies zero polynomials and the degree and monicity of every nonzero represented polynomial.

theorem Complexity.BitPolynomial.Internal.significantLength_le (bits : List Bool) : significantLength bits ≤ bits.length

theorem Complexity.BitPolynomial.Internal.bit_eq_false_of_significantLength_le (bits : List Bool) (i : ℕ) (hi : significantLength bits ≤ i) : bits[i]?.getD false = false

theorem Complexity.BitPolynomial.Internal.bit_at_significantLength (bits : List Bool) (h : 0 < significantLength bits) : bits[significantLength bits - 1]?.getD false = true

theorem Complexity.BitPolynomial.Internal.significantLength_eq_zero_iff (bits : List Bool) : significantLength bits = 0 ↔ ofBits bits = 0

theorem Complexity.BitPolynomial.Internal.ofBits_isMonicOfDegree (bits : List Bool) (h : 0 < significantLength bits) : (ofBits bits).IsMonicOfDegree (significantLength bits - 1)