Keyed unsigned minimum -- proof internals

theorem Complexity.Circuit.eval_unsignedLEWithKeyedPayload_internal (keyWidth payloadWidth : ℕ) [NeZero keyWidth] (leftKey : BitString keyWidth) (leftPayload : BitString payloadWidth) (rightKey : BitString keyWidth) (rightPayload : BitString payloadWidth) : (unsignedLEWithKeyedPayload keyWidth payloadWidth).eval (leftKey.keyedMinimumInput leftPayload rightKey rightPayload) = BitString.multiplexerInput (decide (leftKey.unsignedValue ≤ rightKey.unsignedValue)) (Fin.append leftKey leftPayload) (Fin.append rightKey rightPayload)

theorem Complexity.Circuit.eval_unsignedKeyedMin_internal (keyWidth payloadWidth : ℕ) [NeZero keyWidth] (leftKey : BitString keyWidth) (leftPayload : BitString payloadWidth) (rightKey : BitString keyWidth) (rightPayload : BitString payloadWidth) : (unsignedKeyedMin keyWidth payloadWidth).eval (leftKey.keyedMinimumInput leftPayload rightKey rightPayload) = leftKey.unsignedKeyedMin leftPayload rightKey rightPayload