In the middle of proof, but some useful new lemmas.
Temporary state, may come back to this.
Warning, everything is in a sort of inconsistent state.