@wmansky I moved the incomplete proof to this MR. Once the proof is clear of admits it can be merged. This keeps the main development from having to maintain incomplete proofs.