Unsigned binary minimum -- proof internals

theorem Complexity.BitString.unsignedValue_unsignedMin_internal {width : ℕ} (left right : BitString width) : (left.unsignedMin right).unsignedValue = min left.unsignedValue right.unsignedValue

theorem Complexity.Circuit.eval_unsignedLEWithPayload_internal (width : ℕ) [NeZero width] (left right : BitString width) : (unsignedLEWithPayload width).eval (Fin.append left right) = BitString.multiplexerInput (decide (left.unsignedValue ≤ right.unsignedValue)) left right

theorem Complexity.Circuit.eval_unsignedMin_internal (width : ℕ) [NeZero width] (left right : BitString width) : (unsignedMin width).eval (Fin.append left right) = left.unsignedMin right