Correctness and bounds for binary-polynomial remainder

The scan maintains the monic remainder of the coefficients already read. Its fixed width gives a state bound independent of the dividend length, and the outer zero-modulus branch agrees with Polynomial.modByMonic_zero.

theorem Complexity.BitPolynomial.Internal.remainderScan_length (modulus a : List Bool) : (remainderScan modulus a).length = significantLength modulus - 1

theorem Complexity.BitPolynomial.Internal.remainderScan_correct (modulus a : List Bool) (hm : 0 < significantLength modulus) : ofBits (remainderScan modulus a) = ofBits a %ₘ ofBits modulus

theorem Complexity.BitPolynomial.Internal.remainderBits_length (a modulus : List Bool) : (remainderBits a modulus).length = if significantLength modulus = 0 then a.length else significantLength modulus - 1

theorem Complexity.BitPolynomial.Internal.remainderBits_length_le (a modulus : List Bool) : (remainderBits a modulus).length ≤ max a.length modulus.length

theorem Complexity.BitPolynomial.Internal.ofBits_remainderBits (a modulus : List Bool) : ofBits (remainderBits a modulus) = ofBits a %ₘ ofBits modulus